//===-- Executor.cpp ------------------------------------------------------===//
//
//                     The KLEE Symbolic Virtual Machine
//
// This file is distributed under the University of Illinois Open Source
// License. See LICENSE.TXT for details.
//
//===----------------------------------------------------------------------===//

#include "Common.h"

#include "Executor.h"
 
#include "Context.h"
#include "CoreStats.h"
#include "ExternalDispatcher.h"
#include "ImpliedValue.h"
#include "Memory.h"
#include "MemoryManager.h"
#include "PTree.h"
#include "Searcher.h"
#include "SeedInfo.h"
#include "SpecialFunctionHandler.h"
#include "StatsTracker.h"
#include "TimingSolver.h"
#include "UserSearcher.h"
#include "../Solver/SolverStats.h"
#include "../Module/Passes.h"

#include "BcLib.h"
#include "tern/RaceDetector.h"
#include "xiaowei/Slicer.h"

#include "klee/ExecutionState.h"
#include "klee/Expr.h"
#include "klee/Interpreter.h"
#include "klee/TimerStatIncrementer.h"
#include "klee/util/Assignment.h"
#include "klee/util/ExprPPrinter.h"
#include "klee/util/ExprUtil.h"
#include "klee/Config/config.h"
#include "klee/Internal/ADT/KTest.h"
#include "klee/Internal/ADT/RNG.h"
#include "klee/Internal/Module/Cell.h"
#include "klee/Internal/Module/InstructionInfoTable.h"
#include "klee/Internal/Module/KInstruction.h"
#include "klee/Internal/Module/KModule.h"
#include "klee/Internal/Support/FloatEvaluation.h"
#include "klee/Internal/System/Time.h"

#include "llvm/Attributes.h"
#include "llvm/BasicBlock.h"
#include "llvm/Constants.h"
#include "llvm/Function.h"
#include "llvm/Instructions.h"
#include "llvm/IntrinsicInst.h"
#if !(LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 7)
#include "llvm/LLVMContext.h"
#endif
#include "llvm/Module.h"
#include "llvm/ADT/StringExtras.h"
#include "llvm/Support/CallSite.h"
#include "llvm/Support/CommandLine.h"
#include "llvm/Support/GetElementPtrTypeIterator.h"
#include "llvm/Support/raw_ostream.h"
#include "llvm/System/Process.h"
#include "llvm/Target/TargetData.h"
#include "llvm/PassManager.h"

#include <cassert>
#include <algorithm>
#include <iostream>
#include <iomanip>
#include <fstream>
#include <sstream>
#include <vector>
#include <string>

#include <sys/mman.h>

#include <errno.h>
#include <cxxabi.h>

#include <setjmp.h>
#include <pthread.h>
#include <semaphore.h>
#include <ext/hash_map>
#include <fcntl.h>

using namespace __gnu_cxx;
using namespace llvm;
using namespace klee;

namespace {
  cl::opt<bool>
  DumpStatesOnHalt("dump-states-on-halt",
                   cl::init(true));
 
  cl::opt<bool>
  NoPreferCex("no-prefer-cex",
              cl::init(false));
 
  cl::opt<bool>
  UseAsmAddresses("use-asm-addresses",
                  cl::init(false));
 
  cl::opt<bool>
  RandomizeFork("randomize-fork",
                cl::init(false));
 
  cl::opt<bool>
  AllowExternalSymCalls("allow-external-sym-calls",
                        cl::init(false));

  cl::opt<bool>
  DebugPrintInstructions("debug-print-instructions", 
                         cl::desc("Print instructions during execution."));

  cl::opt<bool>
  DebugCheckForImpliedValues("debug-check-for-implied-values");


  cl::opt<bool>
  SimplifySymIndices("simplify-sym-indices",
                     cl::init(false));

  cl::opt<unsigned>
  MaxSymArraySize("max-sym-array-size",
                  cl::init(0));

  cl::opt<bool>
  DebugValidateSolver("debug-validate-solver",
		      cl::init(false));

  cl::opt<bool>
  SuppressExternalWarnings("suppress-external-warnings");

  cl::opt<bool>
  AllExternalWarnings("all-external-warnings");

  cl::opt<bool>
  OnlyOutputStatesCoveringNew("only-output-states-covering-new",
                              cl::init(false));

  cl::opt<bool>
  AlwaysOutputSeeds("always-output-seeds",
                              cl::init(true));

  cl::opt<bool>
  UseFastCexSolver("use-fast-cex-solver",
		   cl::init(false));

  cl::opt<bool>
  UseIndependentSolver("use-independent-solver",
                       cl::init(true),
		       cl::desc("Use constraint independence"));

  cl::opt<bool>
  EmitAllErrors("emit-all-errors",
                cl::init(false),
                cl::desc("Generate tests cases for all errors "
                         "(default=one per (error,instruction) pair)"));

  cl::opt<bool>
  UseCexCache("use-cex-cache",
              cl::init(true),
	      cl::desc("Use counterexample caching"));

  cl::opt<bool>
  UseQueryPCLog("use-query-pc-log",
                cl::init(false));
  
  cl::opt<bool>
  UseSTPQueryPCLog("use-stp-query-pc-log",
                   cl::init(false));

  cl::opt<bool>
  NoExternals("no-externals", 
           cl::desc("Do not allow external functin calls"));

  cl::opt<bool>
  UseCache("use-cache",
	   cl::init(true),
	   cl::desc("Use validity caching"));

  cl::opt<bool>
  OnlyReplaySeeds("only-replay-seeds", 
                  cl::desc("Discard states that do not have a seed."));
 
  cl::opt<bool>
  OnlySeed("only-seed", 
           cl::desc("Stop execution after seeding is done without doing regular search."));
 
  cl::opt<bool>
  AllowSeedExtension("allow-seed-extension", 
                     cl::desc("Allow extra (unbound) values to become symbolic during seeding."));
 
  cl::opt<bool>
  ZeroSeedExtension("zero-seed-extension");
 
  cl::opt<bool>
  AllowSeedTruncation("allow-seed-truncation", 
                      cl::desc("Allow smaller buffers than in seeds."));
 
  cl::opt<bool>
  NamedSeedMatching("named-seed-matching",
                    cl::desc("Use names to match symbolic objects to inputs."));

  cl::opt<double>
  MaxStaticForkPct("max-static-fork-pct", cl::init(1.));
  cl::opt<double>
  MaxStaticSolvePct("max-static-solve-pct", cl::init(1.));
  cl::opt<double>
  MaxStaticCPForkPct("max-static-cpfork-pct", cl::init(1.));
  cl::opt<double>
  MaxStaticCPSolvePct("max-static-cpsolve-pct", cl::init(1.));

  cl::opt<double>
  MaxInstructionTime("max-instruction-time",
                     cl::desc("Only allow a single instruction to take this much time (default=0 (off))"),
                     cl::init(0));
  
  cl::opt<double>
  SeedTime("seed-time",
           cl::desc("Amount of time to dedicate to seeds, before normal search (default=0 (off))"),
           cl::init(0));
  
  cl::opt<double>
  MaxSTPTime("max-stp-time",
             cl::desc("Maximum amount of time for a single query (default=120s)"),
             cl::init(120.0));
  
  cl::opt<unsigned int>
  StopAfterNInstructions("stop-after-n-instructions",
                         cl::desc("Stop execution after specified number of instructions (0=off)"),
                         cl::init(0));
  
  cl::opt<unsigned>
  MaxForks("max-forks",
           cl::desc("Only fork this many times (-1=off)"),
           cl::init(~0u));
  
  cl::opt<unsigned>
  MaxDepth("max-depth",
           cl::desc("Only allow this many symbolic branches (0=off)"),
           cl::init(0));
  
  cl::opt<unsigned>
  MaxMemory("max-memory",
            cl::desc("Refuse to fork when more above this about of memory (in MB, 0=off)"),
            cl::init(0));

  cl::opt<bool>
  MaxMemoryInhibit("max-memory-inhibit",
            cl::desc("Inhibit forking at memory cap (vs. random terminate)"),
            cl::init(true));

  cl::opt<bool>
  UseForkedSTP("use-forked-stp", 
                 cl::desc("Run STP in forked process"));

  cl::opt<bool>
  STPOptimizeDivides("stp-optimize-divides", 
                 cl::desc("Optimize constant divides into add/shift/multiplies before passing to STP"),
                 cl::init(true));



  //Xiaowei slicer input
  cl::opt<unsigned long long,false,klee::SlicerExploitParser>
  SlicerExploit ("slicer-exploit-ins",
              cl::desc("The unique instruction id in execution trace for the slicer to compute"),
              cl::init(0));

  cl::opt<std::string>
    SlicerOutput ("slicer-output-file",
                cl::desc("Output file for slice"),
                cl::init(""));

}


//static void *theMMap = 0;
//static unsigned theMMapSize = 0;
Executor *executor;
int pthread_create_running;
AddressSpace *sharedAddrSpace;
extern pid_t gettid();
extern pid_t getCnt();

namespace klee {
  RNG theRNG;
}

Solver *constructSolverChain(STPSolver *stpSolver,
                             std::string queryLogPath,
                             std::string stpQueryLogPath,
                             std::string queryPCLogPath,
                             std::string stpQueryPCLogPath) {
  Solver *solver = stpSolver;

  if (UseSTPQueryPCLog)
    solver = createPCLoggingSolver(solver, 
                                   stpQueryLogPath);

  if (UseFastCexSolver)
    solver = createFastCexSolver(solver);

  if (UseCexCache)
    solver = createCexCachingSolver(solver);

  if (UseCache)
    solver = createCachingSolver(solver);

  if (UseIndependentSolver)
    solver = createIndependentSolver(solver);

  if (DebugValidateSolver)
    solver = createValidatingSolver(solver, stpSolver);

  if (UseQueryPCLog)
    solver = createPCLoggingSolver(solver, 
                                   queryPCLogPath);
  
  return solver;
}

Executor::Executor(const InterpreterOptions &opts,
                   InterpreterHandler *ih) 
  : Interpreter(opts),
    kmodule(0),
    interpreterHandler(ih),
    searcher(0),
    externalDispatcher(new ExternalDispatcher()),
    statsTracker(0),
    pathWriter(0),
    symPathWriter(0),
    specialFunctionHandler(0),
    processTree(0),
    replayOut(0),
    replayPath(0),    
    usingSeeds(0),
    atMemoryLimit(false),
    inhibitForking(false),
    haltExecution(false),
    ivcEnabled(false),
    stpTimeout(MaxSTPTime != 0 && MaxInstructionTime != 0
      ? std::min(MaxSTPTime,MaxInstructionTime)
      : std::max(MaxSTPTime,MaxInstructionTime)) {
  STPSolver *stpSolver = new STPSolver(UseForkedSTP, STPOptimizeDivides);
  Solver *solver = 
    constructSolverChain(stpSolver,
                         interpreterHandler->getOutputFilename("queries.qlog"),
                         interpreterHandler->getOutputFilename("stp-queries.qlog"),
                         interpreterHandler->getOutputFilename("queries.pc"),
                         interpreterHandler->getOutputFilename("stp-queries.pc"));
  
  this->solver = new TimingSolver(solver, stpSolver);

  memory = new MemoryManager();
  instCount = 0;
}


const Module *Executor::setModule(llvm::Module *module, 
                                  const ModuleOptions &opts) {
  assert(!kmodule && module && "can only register one module"); // XXX gross
  
  kmodule = new KModule(module);

  // Initialize the context.
  TargetData *TD = kmodule->targetData;
  Context::initialize(TD->isLittleEndian(),
                      (Expr::Width) TD->getPointerSizeInBits());

  specialFunctionHandler = new SpecialFunctionHandler(*this);
  bclib = new BcLib(*this);

  specialFunctionHandler->prepare();
  kmodule->prepare(opts, interpreterHandler);
  specialFunctionHandler->bind();

  if (StatsTracker::useStatistics()) {
    statsTracker = 
      new StatsTracker(*this,
                       interpreterHandler->getOutputFilename("assembly.ll"),
                       userSearcherRequiresMD2U());
  }
  
  return module;
}

Executor::~Executor() {
  delete memory;
  delete externalDispatcher;
  if (processTree)
    delete processTree;
  if (specialFunctionHandler)
    delete specialFunctionHandler;
  if (statsTracker)
    delete statsTracker;
  delete solver;
  delete kmodule;
}

/***/

void Executor::initializeGlobalObject(ExecutionState &state, ObjectState *os,
                                      Constant *c, 
                                      unsigned offset) {
  TargetData *targetData = kmodule->targetData;
  if (ConstantVector *cp = dyn_cast<ConstantVector>(c)) {
    unsigned elementSize =
      targetData->getTypeStoreSize(cp->getType()->getElementType());
    for (unsigned i=0, e=cp->getNumOperands(); i != e; ++i)
      initializeGlobalObject(state, os, cp->getOperand(i), 
			     offset + i*elementSize);
  } else if (isa<ConstantAggregateZero>(c)) {
    unsigned i, size = targetData->getTypeStoreSize(c->getType());
    for (i=0; i<size; i++)
      os->write8(offset+i, (uint8_t) 0);
  } else if (ConstantArray *ca = dyn_cast<ConstantArray>(c)) {
    unsigned elementSize =
      targetData->getTypeStoreSize(ca->getType()->getElementType());
    for (unsigned i=0, e=ca->getNumOperands(); i != e; ++i)
      initializeGlobalObject(state, os, ca->getOperand(i), 
			     offset + i*elementSize);
  } else if (ConstantStruct *cs = dyn_cast<ConstantStruct>(c)) {
    const StructLayout *sl =
      targetData->getStructLayout(cast<StructType>(cs->getType()));
    for (unsigned i=0, e=cs->getNumOperands(); i != e; ++i)
      initializeGlobalObject(state, os, cs->getOperand(i), 
			     offset + sl->getElementOffset(i));
  } else {
    unsigned StoreBits = targetData->getTypeStoreSizeInBits(c->getType());
    ref<ConstantExpr> C = evalConstant(c);

    // Extend the constant if necessary;
    assert(StoreBits >= C->getWidth() && "Invalid store size!");
    if (StoreBits > C->getWidth())
      C = C->ZExt(StoreBits);

    os->write(offset, C);
    // Heming
    os->writeConcrete(offset, C);
  }
}

MemoryObject * Executor::addExternalObject(ExecutionState &state, 
                                           void *addr, unsigned size, 
                                           bool isReadOnly) {
  MemoryObject *mo = memory->allocateFixed((uint64_t) (unsigned long) addr, 
                                           size, 0);
  ObjectState *os = bindObjectInState(state, mo, false);
  for(unsigned i = 0; i < size; i++)
    os->write8Direct(i, ((uint8_t*)addr)[i]);
//    os->write8(i, ((uint8_t*)addr)[i]);
  if(isReadOnly)
    os->setReadOnly(true);  
  return mo;
}

void Executor::initializeGlobals(ExecutionState &state) {
  Module *m = kmodule->module;

  if (m->getModuleInlineAsm() != "")
    klee_warning("executable has module level assembly (ignoring)");

  assert(m->lib_begin() == m->lib_end() &&
         "XXX do not support dependent libraries");

  // represent function globals using the address of the actual llvm function
  // object. given that we use malloc to allocate memory in states this also
  // ensures that we won't conflict. we don't need to allocate a memory object
  // since reading/writing via a function pointer is unsupported anyway.
  for (Module::iterator i = m->begin(), ie = m->end(); i != ie; ++i) {
    Function *f = i;
    ref<ConstantExpr> addr(0);

    // If the symbol has external weak linkage then it is implicitly
    // not defined in this module; if it isn't resolvable then it
    // should be null.
    if (f->hasExternalWeakLinkage() && 
        !externalDispatcher->resolveSymbol(f->getNameStr())) {
      addr = Expr::createPointer(0);
    } else {
      addr = Expr::createPointer((unsigned long) (void*) f);
      legalFunctions.insert((uint64_t) (unsigned long) (void*) f);
    }
    
    globalAddresses.insert(std::make_pair(f, addr));
  }

  // Disabled, we don't want to promote use of live externals.
#ifdef HAVE_CTYPE_EXTERNALS
#ifndef WINDOWS
#ifndef DARWIN
  /* From /usr/include/errno.h: it [errno] is a per-thread variable. */
/*  int *errno_addr = __errno_location();
  addExternalObject(state, (void *)errno_addr, sizeof *errno_addr, false);
*/
  /* from /usr/include/ctype.h:
       These point into arrays of 384, so they can be indexed by any `unsigned
       char' value [0,255]; by EOF (-1); or by any `signed char' value
       [-128,-1).  ISO C requires that the ctype functions work for `unsigned */
/*  const uint16_t **addr = __ctype_b_loc();
  addExternalObject(state, (void *)(*addr-128), 
                    384 * sizeof **addr, true);
  addExternalObject(state, addr, sizeof(*addr), true);
    
  const int32_t **lower_addr = __ctype_tolower_loc();
  addExternalObject(state, (void *)(*lower_addr-128), 
                    384 * sizeof **lower_addr, true);
  addExternalObject(state, lower_addr, sizeof(*lower_addr), true);
  
  const int32_t **upper_addr = __ctype_toupper_loc();
  addExternalObject(state, (void *)(*upper_addr-128), 
                    384 * sizeof **upper_addr, true);
  addExternalObject(state, upper_addr, sizeof(*upper_addr), true);*/
#endif
#endif
#endif

  // allocate and initialize globals, done in two passes since we may
  // need address of a global in order to initialize some other one.

  // allocate memory objects for all globals
  for (Module::const_global_iterator i = m->global_begin(),
         e = m->global_end();
       i != e; ++i) {
    if (i->isDeclaration()) {
      // FIXME: We have no general way of handling unknown external
      // symbols. If we really cared about making external stuff work
      // better we could support user definition, or use the EXE style
      // hack where we check the object file information.

      const Type *ty = i->getType()->getElementType();
      uint64_t size = kmodule->targetData->getTypeStoreSize(ty);

      // XXX - DWD - hardcode some things until we decide how to fix.
#ifndef WINDOWS
      if (i->getName() == "_ZTVN10__cxxabiv117__class_type_infoE") {
        size = 0x2C;
      } else if (i->getName() == "_ZTVN10__cxxabiv120__si_class_type_infoE") {
        size = 0x2C;
      } else if (i->getName() == "_ZTVN10__cxxabiv121__vmi_class_type_infoE") {
        size = 0x2C;
      }
#endif

      if (size == 0) {
        llvm::errs() << "Unable to find size for global variable: " 
                     << i->getName() 
                     << " (use will result in out of bounds access)\n";
      }

      MemoryObject *mo = memory->allocate(size, false, true, i);
      ObjectState *os = bindObjectInState(state, mo, false);
      globalObjects.insert(std::make_pair(i, mo));
      globalAddresses.insert(std::make_pair(i, mo->getBaseExpr()));

      // Program already running = object already initialized.  Read
      // concrete value and write it to our copy.
      if (size) {
        void *addr;
        if (i->getName() == "__dso_handle") {
          extern void *__dso_handle __attribute__ ((__weak__));
          addr = &__dso_handle; // wtf ?
        } else {
          addr = externalDispatcher->resolveSymbol(i->getNameStr());
        }
        if (!addr)
          klee_error("unable to load symbol(%s) while initializing globals.", 
                     i->getName().data());

        for (unsigned offset=0; offset<mo->size; offset++)
          os->write8(offset, ((unsigned char*)addr)[offset]);
      }
    } else {
      const Type *ty = i->getType()->getElementType();
      uint64_t size = kmodule->targetData->getTypeStoreSize(ty);
      MemoryObject *mo = 0;

      if (UseAsmAddresses && i->getName()[0]=='\01') {
        char *end;
        uint64_t address = ::strtoll(i->getNameStr().c_str()+1, &end, 0);

        if (end && *end == '\0') {
          klee_message("NOTE: allocated global at asm specified address: %#08llx"
                       " (%llu bytes)",
                       (long long) address, (unsigned long long) size);
          mo = memory->allocateFixed(address, size, &*i);
          mo->isUserSpecified = true; // XXX hack;
        }
      }

      if (!mo)
        mo = memory->allocate(size, false, true, &*i);
      assert(mo && "out of memory");
      ObjectState *os = bindObjectInState(state, mo, false);
      globalObjects.insert(std::make_pair(i, mo));
      globalAddresses.insert(std::make_pair(i, mo->getBaseExpr()));

      if (!i->hasInitializer())
          os->initializeToRandom();
    }
  }
  
  // link aliases to their definitions (if bound)
  for (Module::alias_iterator i = m->alias_begin(), ie = m->alias_end(); 
       i != ie; ++i) {
    // Map the alias to its aliasee's address. This works because we have
    // addresses for everything, even undefined functions. 
    globalAddresses.insert(std::make_pair(i, evalConstant(i->getAliasee())));
  }

  // once all objects are allocated, do the actual initialization
  for (Module::const_global_iterator i = m->global_begin(),
         e = m->global_end();
       i != e; ++i) {
    if (i->hasInitializer()) {
      MemoryObject *mo = globalObjects.find(i)->second;
      const ObjectState *os = state.addressSpace.findObject(mo);
      long int_os2 = (long)os;
      ObjectState *os2 = (ObjectState *)int_os2;
      assert(os2);
      ObjectState *wos = state.addressSpace.getWriteable(mo, os2);
      
      initializeGlobalObject(state, wos, i->getInitializer(), 0);
      // if(i->isConstant()) os->setReadOnly(true);
    }
  }
}

void Executor::branch(ExecutionState &state, 
                      const std::vector< ref<Expr> > &conditions,
                      std::vector<ExecutionState*> &result) {
  TimerStatIncrementer timer(*stats::forkTime);
  unsigned N = conditions.size();
  assert(N);

  *stats::forks += N-1;

  // XXX do proper balance or keep random?
  result.push_back(&state);
  for (unsigned i=1; i<N; ++i) {
    // Heming disables this branch.
    assert(false);
    ExecutionState *es = result[theRNG.getInt32() % i];
    ExecutionState *ns = es->branch();
    addedStates.insert(ns);
    result.push_back(ns);
    es->ptreeNode->data = 0;
    std::pair<PTree::Node*,PTree::Node*> res = 
      processTree->split(es->ptreeNode, ns, es);
    ns->ptreeNode = res.first;
    es->ptreeNode = res.second;
  }

  // If necessary redistribute seeds to match conditions, killing
  // states if necessary due to OnlyReplaySeeds (inefficient but
  // simple).
  
  std::map< ExecutionState*, std::vector<SeedInfo> >::iterator it = 
    seedMap.find(&state);
  if (it != seedMap.end()) {
    std::vector<SeedInfo> seeds = it->second;
    seedMap.erase(it);

    // Assume each seed only satisfies one condition (necessarily true
    // when conditions are mutually exclusive and their conjunction is
    // a tautology).
    for (std::vector<SeedInfo>::iterator siit = seeds.begin(), 
           siie = seeds.end(); siit != siie; ++siit) {
      unsigned i;
      for (i=0; i<N; ++i) {
        ref<ConstantExpr> res;
        bool success = 
          solver->getValue(state, siit->assignment.evaluate(conditions[i]), 
                           res);
        assert(success && "FIXME: Unhandled solver failure");
        (void) success;
        if (res->isTrue())
          break;
      }
      
      // If we didn't find a satisfying condition randomly pick one
      // (the seed will be patched).
      if (i==N)
        i = theRNG.getInt32() % N;

      seedMap[result[i]].push_back(*siit);
    }

    if (OnlyReplaySeeds) {
      for (unsigned i=0; i<N; ++i) {
        if (!seedMap.count(result[i])) {
          terminateState(*result[i]);
          result[i] = NULL;
        }
      } 
    }
  }

  for (unsigned i=0; i<N; ++i)
    if (result[i])
      addConstraint(*result[i], conditions[i]);
}

void Executor::printFunctionAndBB(ExecutionState &state, const char *info) {
  fprintf(stderr, "printFunctionAndBB %s at function %s, bb %s\n", info,
		state.prevPC->inst->getParent()->getParent()->getNameStr().c_str(),
		state.prevPC->inst->getParent()->getNameStr().c_str());
  //std::cerr << "Inst " << *(state.prevPC->inst) << "\n\n";  
}

Executor::StatePair 
Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal, ref<Expr> *concrete_condition) {
  Solver::Validity res;
  std::map< ExecutionState*, std::vector<SeedInfo> >::iterator it = 
    seedMap.find(&current);
  bool isSeeding = it != seedMap.end();

  if (!isSeeding && !isa<ConstantExpr>(condition) && 
      (MaxStaticForkPct!=1. || MaxStaticSolvePct != 1. ||
       MaxStaticCPForkPct!=1. || MaxStaticCPSolvePct != 1.) /*&&
      statsTracker->elapsed() > 60.*/) {
    StatisticManager &sm = *theStatisticManager;
    CallPathNode *cpn = current.stack.back().callPathNode;
    if ((MaxStaticForkPct<1. &&
         sm.getIndexedValue(*stats::forks, sm.getIndex()) > 
         *stats::forks*MaxStaticForkPct) ||
        (MaxStaticCPForkPct<1. &&
         cpn && (cpn->statistics.getValue(*stats::forks) > 
                 *stats::forks*MaxStaticCPForkPct)) ||
        (MaxStaticSolvePct<1 &&
         sm.getIndexedValue(*stats::solverTime, sm.getIndex()) > 
         *stats::solverTime*MaxStaticSolvePct) ||
        (MaxStaticCPForkPct<1. &&
         cpn && (cpn->statistics.getValue(*stats::solverTime) > 
                 *stats::solverTime*MaxStaticCPSolvePct))) {
      ref<ConstantExpr> value; 
      bool success = solver->getValue(current, condition, value);
      assert(success && "FIXME: Unhandled solver failure");
      (void) success;
      addConstraint(current, EqExpr::create(value, condition));
      condition = value;
    }      
  }

  double timeout = stpTimeout;
  if (isSeeding)
    timeout *= it->second.size();
  solver->setTimeout(timeout);
//  bool success = solver->evaluate(current, condition, res);
	bool success;
	// Heming: do not solve any constraint here in order to save time.
  if (isa<ConstantExpr>(condition))
    success = solver->evaluate(current, condition, res);
  else {
    success = true;
    res = Solver::Unknown;
  }
  solver->setTimeout(0);
  if (!success) {
    current.pc = current.prevPC;
    terminateStateEarly(current, "query timed out");
    return StatePair(0, 0);
  }

  if (!isSeeding) {
    if (replayPath && !isInternal) {
      assert(replayPosition<replayPath->size() &&
             "ran out of branches in replay path mode");
      bool branch = (*replayPath)[replayPosition++];
      
      if (res==Solver::True) {
        assert(branch && "hit invalid branch in replay path mode");
      } else if (res==Solver::False) {
        assert(!branch && "hit invalid branch in replay path mode");
      } else {
        // add constraints
        if(branch) {
          res = Solver::True;
          addConstraint(current, condition);
        } else  {
          res = Solver::False;
          addConstraint(current, Expr::createIsZero(condition));
        }
      }
    } else if (res==Solver::Unknown) {
      assert(!replayOut && "in replay mode, only one branch can be true.");
      
      if ((MaxMemoryInhibit && atMemoryLimit) || 
          current.forkDisabled ||
          inhibitForking || 
          (MaxForks!=~0u && *stats::forks >= MaxForks)) {

	if (MaxMemoryInhibit && atMemoryLimit)
	  klee_warning_once(0, "skipping fork (memory cap exceeded)");
	else if (current.forkDisabled)
	  klee_warning_once(0, "skipping fork (fork disabled on current path)");
	else if (inhibitForking)
	  klee_warning_once(0, "skipping fork (fork disabled globally)");
	else 
	  klee_warning_once(0, "skipping fork (max-forks reached)");

        TimerStatIncrementer timer(*stats::forkTime);
        if (theRNG.getBool()) {
          addConstraint(current, condition);
          res = Solver::True;        
        } else {
          addConstraint(current, Expr::createIsZero(condition));
          res = Solver::False;
        }
      }
    }
  }

  // Fix branch in only-replay-seed mode, if we don't have both true
  // and false seeds.
  if (isSeeding && 
      (current.forkDisabled || OnlyReplaySeeds) && 
      res == Solver::Unknown) {
    bool trueSeed=false, falseSeed=false;
    // Is seed extension still ok here?
    for (std::vector<SeedInfo>::iterator siit = it->second.begin(), 
           siie = it->second.end(); siit != siie; ++siit) {
      ref<ConstantExpr> res;
      bool success = 
        solver->getValue(current, siit->assignment.evaluate(condition), res);
      assert(success && "FIXME: Unhandled solver failure");
      (void) success;
      if (res->isTrue()) {
        trueSeed = true;
      } else {
        falseSeed = true;
      }
      if (trueSeed && falseSeed)
        break;
    }
    if (!(trueSeed && falseSeed)) {
      assert(trueSeed || falseSeed);
      
      res = trueSeed ? Solver::True : Solver::False;
      addConstraint(current, trueSeed ? condition : Expr::createIsZero(condition));
    }
  }


  // XXX - even if the constraint is provable one way or the other we
  // can probably benefit by adding this constraint and allowing it to
  // reduce the other constraints. For example, if we do a binary
  // search on a particular value, and then see a comparison against
  // the value it has been fixed at, we should take this as a nice
  // hint to just use the single constraint instead of all the binary
  // search ones. If that makes sense.
  if (res==Solver::True) {
    if (!isInternal) {
      if (pathWriter) {
        current.pathOS << "1";
      }
    }

    return StatePair(&current, 0);
  } else if (res==Solver::False) {
    if (!isInternal) {
      if (pathWriter) {
        current.pathOS << "0";
      }
    }

    return StatePair(0, &current);
  } else {
    TimerStatIncrementer timer(*stats::forkTime);
    ExecutionState *falseState, *trueState = &current;
/*
    ++stats::forks;

    falseState = trueState->branch();
    addedStates.insert(falseState);

    if (RandomizeFork && theRNG.getBool())
      std::swap(trueState, falseState);

    if (it != seedMap.end()) {
      std::vector<SeedInfo> seeds = it->second;
      it->second.clear();
      std::vector<SeedInfo> &trueSeeds = seedMap[trueState];
      std::vector<SeedInfo> &falseSeeds = seedMap[falseState];
      for (std::vector<SeedInfo>::iterator siit = seeds.begin(), 
             siie = seeds.end(); siit != siie; ++siit) {
        ref<ConstantExpr> res;
        bool success = 
          solver->getValue(current, siit->assignment.evaluate(condition), res);
        assert(success && "FIXME: Unhandled solver failure");
        (void) success;
        if (res->isTrue()) {
          trueSeeds.push_back(*siit);
        } else {
          falseSeeds.push_back(*siit);
        }
      }
      
      bool swapInfo = false;
      if (trueSeeds.empty()) {
        if (&current == trueState) swapInfo = true;
        seedMap.erase(trueState);
      }
      if (falseSeeds.empty()) {
        if (&current == falseState) swapInfo = true;
        seedMap.erase(falseState);
      }
      if (swapInfo) {
        std::swap(trueState->coveredNew, falseState->coveredNew);
        std::swap(trueState->coveredLines, falseState->coveredLines);
      }
    }

    current.ptreeNode->data = 0;
    std::pair<PTree::Node*, PTree::Node*> res =
      processTree->split(current.ptreeNode, falseState, trueState);
    falseState->ptreeNode = res.first;
    trueState->ptreeNode = res.second;

    if (!isInternal) {
      if (pathWriter) {
        falseState->pathOS = pathWriter->open(current.pathOS);
        trueState->pathOS << "1";
        falseState->pathOS << "0";
      }      
      if (symPathWriter) {
        falseState->symPathOS = symPathWriter->open(current.symPathOS);
        trueState->symPathOS << "1";
        falseState->symPathOS << "0";
      }
    }

    addConstraint(*trueState, condition);
    addConstraint(*falseState, Expr::createIsZero(condition));
*/


    ++*stats::forks;

    // Heming change this, we even do not need to fork any new state for branch.
    falseState = trueState;

    if (RandomizeFork && theRNG.getBool())
      std::swap(trueState, falseState);

    if (it != seedMap.end()) {
      std::vector<SeedInfo> seeds = it->second;
      it->second.clear();
      std::vector<SeedInfo> &trueSeeds = seedMap[trueState];
      std::vector<SeedInfo> &falseSeeds = seedMap[falseState];
      for (std::vector<SeedInfo>::iterator siit = seeds.begin(), 
             siie = seeds.end(); siit != siie; ++siit) {
        ref<ConstantExpr> res;
        bool success = 
          solver->getValue(current, siit->assignment.evaluate(condition), res);
        assert(success && "FIXME: Unhandled solver failure");
        (void) success;
        if (res->isTrue()) {
          trueSeeds.push_back(*siit);
        } else {
          falseSeeds.push_back(*siit);
        }
      }
      
      bool swapInfo = false;
      if (trueSeeds.empty()) {
        if (&current == trueState) swapInfo = true;
        seedMap.erase(trueState);
      }
      if (falseSeeds.empty()) {
        if (&current == falseState) swapInfo = true;
        seedMap.erase(falseState);
      }
      if (swapInfo) {
        std::swap(trueState->coveredNew, falseState->coveredNew);
        std::swap(trueState->coveredLines, falseState->coveredLines);
      }
    }

    if (!isInternal) {
      if (pathWriter) {
        falseState->pathOS = pathWriter->open(current.pathOS);
        trueState->pathOS << "1";
        falseState->pathOS << "0";
      }      
      if (symPathWriter) {
        falseState->symPathOS = symPathWriter->open(current.symPathOS);
        trueState->symPathOS << "1";
        falseState->symPathOS << "0";
      }
    }

    if (concrete_condition) {
      assert(isa<ConstantExpr>(*concrete_condition) && "The argument concrete_condition in fork() must be concrete expr.");
      if (!cast<ConstantExpr>(*concrete_condition)->getZExtValue()) {
        //fprintf(stderr, "branch is false\n");
        // Heming: if the concrete condition is false, then just explore the false branch and disable the true branch.
        addConstraint(*falseState, Expr::createIsZero(condition));
        //addedStates.insert(falseState);
        //trueState->isValid = false;
        //removedStates.insert(trueState);
        trueState = NULL;
      } else {
        //fprintf(stderr, "branch is true\n");
        addConstraint(*trueState, condition);
        falseState = NULL;
      }
    } else {
      printKLEECallStack(*trueState);
      assert(false && "TERN fork(), a wrong branch, I do not need this");
      addConstraint(*trueState, condition);
      addConstraint(*falseState, Expr::createIsZero(condition));
      addedStates.insert(falseState);
    }

    // Kinda gross, do we even really still want this option?
    if (MaxDepth && MaxDepth<=trueState->depth) {
      terminateStateEarly(*trueState, "max-depth exceeded");
      terminateStateEarly(*falseState, "max-depth exceeded");
      return StatePair(0, 0);
    }

    return StatePair(trueState, falseState);
  }
}

void Executor::addConstraint(ExecutionState &state, ref<Expr> condition) {
  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(condition)) {
    assert(CE->isTrue() && "attempt to add invalid constraint");
    return;
  }

  // Check to see if this constraint violates seeds.
  std::map< ExecutionState*, std::vector<SeedInfo> >::iterator it = 
    seedMap.find(&state);
  if (it != seedMap.end()) {
    bool warn = false;
    for (std::vector<SeedInfo>::iterator siit = it->second.begin(), 
           siie = it->second.end(); siit != siie; ++siit) {
      bool res;
      bool success = 
        solver->mustBeFalse(state, siit->assignment.evaluate(condition), res);
      assert(success && "FIXME: Unhandled solver failure");
      (void) success;
      if (res) {
        siit->patchSeed(state, condition, solver);
        warn = true;
      }
    }
    if (warn)
      klee_warning("seeds patched for violating constraint"); 
  }

  state.addConstraint(condition);

#ifdef MEMOIZER_ORDER
  if (!isa<BranchInst>(state.prevPC->inst)) {
    fprintf(stderr, "TERN WARN: adding constraint for non branching instructions\n");
  } else {
    BranchInst *branch = dyn_cast<BranchInst>(state.prevPC->inst);
    if (memoizer->omitBranch(branch, condition)) {
      
      return;
    }
  }
  schedCache->addConstraint(0, condition);
#else
// Heming: we do not need to log constraints here, since random schdules equal to record and replay for the same input,
// which do not require any constraints.
#endif

  if (ivcEnabled)
    doImpliedValueConcretization(state, condition, 
                                 ConstantExpr::alloc(1, Expr::Bool));
}

ref<klee::ConstantExpr> Executor::evalConstant(Constant *c) {
  if (llvm::ConstantExpr *ce = dyn_cast<llvm::ConstantExpr>(c)) {
    return evalConstantExpr(ce);
  } else {
    if (const ConstantInt *ci = dyn_cast<ConstantInt>(c)) {
      return ConstantExpr::alloc(ci->getValue());
    } else if (const ConstantFP *cf = dyn_cast<ConstantFP>(c)) {      
      return ConstantExpr::alloc(cf->getValueAPF().bitcastToAPInt());
    } else if (const GlobalValue *gv = dyn_cast<GlobalValue>(c)) {
      return globalAddresses.find(gv)->second;
    } else if (isa<ConstantPointerNull>(c)) {
      return Expr::createPointer(0);
    } else if (isa<UndefValue>(c) || isa<ConstantAggregateZero>(c)) {
      return ConstantExpr::create(0, getWidthForLLVMType(c->getType()));
    } else {
      // Constant{Array,Struct,Vector}
      assert(0 && "invalid argument to evalConstant()");
    }
  }
}


//Xiaowei
void Executor::addEdge(KInstruction *ki, unsigned index,
          ExecutionState &state, TraceEntry * te)
{
	  assert(index < ki->inst->getNumOperands());
	  int vnumber = ki->operands[index];

	  assert(vnumber != -1 &&
	         "Invalid operand to eval(), not a value or constant!");

	  // Determine if this is a constant or not.
	  if (vnumber < 0) {
	    //unsigned index = -vnumber - 2;
	    //return kmodule->constantTable[index];
	  } else {
	    unsigned index = vnumber;
	    StackFrame &sf = state.stack.back();
	    //Xiaowei
	    TraceEntry * useentry = sf.shdwreg[index];
	    te->defuse.insert(useentry);
	    if ( useentry != NULL)
	    	useentry->usedef.insert(te);

	    //return sf.locals[index];
	  }
}

const Cell& Executor::eval(KInstruction *ki, unsigned index, 
                           ExecutionState &state) const {
  assert(index < ki->inst->getNumOperands());
  int vnumber = ki->operands[index];

  assert(vnumber != -1 &&
         "Invalid operand to eval(), not a value or constant!");

  // Determine if this is a constant or not.
  if (vnumber < 0) {
    unsigned index = -vnumber - 2;
    return kmodule->constantTable[index];
  } else {
    unsigned index = vnumber;
    StackFrame &sf = state.stack.back();

    return sf.locals[index];
  }
}

//Xiaowei
void Executor::writeShdwReg(KInstruction *target, ExecutionState &state, TraceEntry *vte)
{
	state.stack.back().shdwreg[target->dest]=vte;
}
void Executor::writeShdwReg(KFunction *kf, unsigned index,
        ExecutionState &state, TraceEntry *vte)
{
	int i = kf->getArgRegister(index);
	state.stack.back().shdwreg[i] = vte;
}

void Executor::bindLocal(KInstruction *target, ExecutionState &state, 
                         ref<Expr> value) {
	//Xiaowei
	writeShdwReg(target,state,slicer->get_cur_te());
	//slicer->printTraceEntry(slicer->get_cur_te());
	//slicer->printTraceEntry(target->te);
	//assert (slicer->get_cur_te() == target->te);
	slicer->get_cur_te()->destvalue = value;
  getDestCell(state, target).value = value;
  if (isa<ConstantExpr>(value)) {
    getDestCell(state, target).concrete_value = value;
    slicer->get_cur_te()->destvalue_concrete = value;
  }
}

void Executor::bindLocalConcrete(KInstruction *target, ExecutionState &state, 
                         ref<Expr> value) {
	//Xiaowei
	writeShdwReg(target,state,slicer->get_cur_te());
	//slicer->printTraceEntry(slicer->get_cur_te());
	//slicer->printTraceEntry(target->te);
	//assert (slicer->get_cur_te() == target->te);
	slicer->get_cur_te()->destvalue_concrete = value;

  assert(isa<ConstantExpr>(value) && "The value argument of bindLocalConcrete must be concrete.");
  //fprintf(stderr, "bindLocalConcrete cell addr %p\n", &(getDestCell(state, target)));
  getDestCell(state, target).concrete_value = value;

}

void Executor::bindArgument(KFunction *kf, unsigned index, 
                            ExecutionState &state, ref<Expr> value) {

	//Xiaowei
	//state.stack.back().shdwreg[kf->getArgRegister(index)]=vte;
	writeShdwReg(kf,index, state, slicer->get_cur_te());
  getArgumentCell(state, kf, index).value = value;
  if (isa<ConstantExpr>(value))
    getArgumentCell(state, kf, index).concrete_value = value;
}

// HEMING. Why?
void Executor::bindArgumentConcrete(KFunction *kf, unsigned index, 
                            ExecutionState &state, ref<Expr> value) {

	//Xiaowei
	//state.stack.back().shdwreg[kf->getArgRegister(index)]=vte;
	writeShdwReg(kf,index, state, slicer->get_cur_te());
  getArgumentCell(state, kf, index).concrete_value = value;
}

ref<Expr> Executor::toUnique(const ExecutionState &state, 
                             ref<Expr> &e) {
  ref<Expr> result = e;

  if (!isa<ConstantExpr>(e)) {
    ref<ConstantExpr> value;
    bool isTrue = false;

    solver->setTimeout(stpTimeout);      
    if (solver->getValue(state, e, value) &&
        solver->mustBeTrue(state, EqExpr::create(e, value), isTrue) &&
        isTrue)
      result = value;
    solver->setTimeout(0);
  }
  
  return result;
}

// Heming: concretize an expression after a task is done.
ref<klee::ConstantExpr> 
Executor::toConcrete(ExecutionState &state, 
                     ref<Expr> e,
                     const char *reason) {
  e = state.constraints.simplifyExpr(e);
  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(e))
    return CE;

  ref<ConstantExpr> value;
  bool success = solver->getValue(state, e, value);
  assert(success && "TERN FIXME: Unhandled solver failure");    
  return value;
}

// Heming: after a task is done, concretize current thread (state).
void Executor::concretizeState(ExecutionState &state) {
#ifdef ENFORCE_WINDOW
  executor_print("concretizeState enter\n");
  // concretize local memory address space.
  for (MemoryMap::iterator it = state.addressSpace.objects.begin(), ie = state.addressSpace.objects.end(); it != ie; ++it) {
    const MemoryObject *mo = it->first;
    const ObjectState *os = it->second;
    if (!os->isKnownSymbolic()) 
      continue;

    long int_os = (long)os;
    ObjectState *os2 = (ObjectState *)int_os;
    ObjectState *newOs = state.addressSpace.getWriteable(mo, os2);
    newOs->makeConcrete();
  }

  // Prepare for assignment.
  std::vector<const Array*> objects;
  for (unsigned i = 0; i < state.symbolics.size(); i++) {
    objects.push_back(state.symbolics[i].second);
  }

  std::vector< std::vector<unsigned char> > values;
  values = std::vector< std::vector<unsigned char> >(objects.size());
  for (unsigned i = 0; i < objects.size(); i++) {
    std::vector<unsigned char> &data = values[i];
    const MemoryObject *mo = state.symbolics[i].first;
    const ObjectState *os = state.addressSpace.findObject(mo);
    // Heming: some local var which works for cache find return function (e.g., cache_find() for httpd) would be already
    // released when the function returned. This is correct.
    if (!os)
      continue;
	
    for (unsigned j = 0; j < os->size; j++) {
      //fprintf(stderr, "push %u to data\n", os->concreteStore[j]);
      data.push_back(os->concreteStore[j]);
    }
  }
  Assignment *binding = new Assignment(objects, values);

  // Simplify expressions at shared addr space.
  for (MemoryMap::iterator it = sharedAddrSpace->objects.begin(), ie = sharedAddrSpace->objects.end(); it != ie; ++it) {
    const MemoryObject *mo = it->first;
    const ObjectState *os = it->second;
    if (!os->isKnownSymbolic()) 
      continue;

    long int_os = (long)os;
    ObjectState *os2 = (ObjectState *)int_os;
    ObjectState *newOs = sharedAddrSpace->getWriteable(mo, os2);
    for (unsigned i = 0; i < newOs->size; i++) {
      if (newOs->isByteKnownSymbolic(i)) {
        ref<Expr> e = newOs->read8(i);
       ref<Expr> e2 = binding->ternEvaluate(e);	// try to concretize part of the expr based on the binding of current state.
	   if (isa<ConstantExpr>(e2)) {
	     newOs->write8(i, cast<ConstantExpr>(e2)->getZExtValue(8));
		 newOs->markByteConcrete(i);
	   } else {
         newOs->write8(i, e2);
	   }
      }
    }
  }

  // remove symbolics.
  state.clearSymbolic();

  // remove constraints.
  state.clearConstraints();
#endif
}

/* Concretize the given expression, and return a possible constant value. 
   'reason' is just a documentation string stating the reason for concretization. */
ref<klee::ConstantExpr> 
Executor::toConstant(ExecutionState &state, 
                     ref<Expr> e,
                     const char *reason) {
  e = state.constraints.simplifyExpr(e);
  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(e))
    return CE;

  ref<ConstantExpr> value;
  bool success = solver->getValue(state, e, value);
  assert(success && "FIXME: Unhandled solver failure");
  (void) success;
    
  std::ostringstream os;
  os << "silently concretizing (reason: " << reason << ") expression " << e 
     << " to value " << value 
     << " (" << (*(state.pc)).info->file << ":" << (*(state.pc)).info->line << ")";
      
  if (AllExternalWarnings)
    klee_warning(reason, os.str().c_str());
  else
    klee_warning_once(reason, "%s", os.str().c_str());

  addConstraint(state, EqExpr::create(e, value));
    
  return value;
}

void Executor::executeGetValue(ExecutionState &state,
                               ref<Expr> e,
                               KInstruction *target) {
  e = state.constraints.simplifyExpr(e);
  std::map< ExecutionState*, std::vector<SeedInfo> >::iterator it = 
    seedMap.find(&state);
  if (it==seedMap.end() || isa<ConstantExpr>(e)) {
    ref<ConstantExpr> value;
    bool success = solver->getValue(state, e, value);
    assert(success && "FIXME: Unhandled solver failure");
    (void) success;
    bindLocal(target, state, value);
  } else {
    std::set< ref<Expr> > values;
    for (std::vector<SeedInfo>::iterator siit = it->second.begin(), 
           siie = it->second.end(); siit != siie; ++siit) {
      ref<ConstantExpr> value;
      bool success = 
        solver->getValue(state, siit->assignment.evaluate(e), value);
      assert(success && "FIXME: Unhandled solver failure");
      (void) success;
      values.insert(value);
    }
    
    std::vector< ref<Expr> > conditions;
    for (std::set< ref<Expr> >::iterator vit = values.begin(), 
           vie = values.end(); vit != vie; ++vit)
      conditions.push_back(EqExpr::create(e, *vit));

    std::vector<ExecutionState*> branches;
    branch(state, conditions, branches);
    
    std::vector<ExecutionState*>::iterator bit = branches.begin();
    for (std::set< ref<Expr> >::iterator vit = values.begin(), 
           vie = values.end(); vit != vie; ++vit) {
      ExecutionState *es = *bit;
      if (es)
        bindLocal(target, *es, *vit);
      ++bit;
    }
  }
}

void Executor::stepInstruction(ExecutionState &state) {
/*  if (DebugPrintInstructions) {
    printFileLine(state, state.pc);
    std::cerr << std::setw(10) << stats::instructions << " ";
    llvm::errs() << *(state.pc->inst);
  }

  if (statsTracker)
    statsTracker->stepInstruction(state);

  ++stats::instructions;
  state.prevPC = state.pc;
  ++state.pc;

  if (stats::instructions==StopAfterNInstructions)
    haltExecution = true;*/

  ++*stats::instructions;
  state.prevPC = state.pc;
  ++state.pc;
  ternInstCntStat(state);
}

void Executor::executeCall(ExecutionState &state, 
                           KInstruction *ki,
                           Function *f,
                           std::vector< ref<Expr> > &arguments, std::vector< ref<Expr> > &concrete_arguments,
                           TraceEntry * te) {

  const char *funcName = f->getNameStr().c_str();
  if (MEMOIZER_PRINT_EXECUTE_CALL
		/*strstr(funcName, "rgetline")  ||
  		strstr(funcName, "_cond_")  || 
		strstr(funcName, "queue")  || 
		strstr(funcName, "http")  || 
		strstr(funcName, "request")  || 
		strstr(funcName, "protocol")  || 
		strstr(funcName, "cache")  || 
		strstr(funcName, "process")  || 
		strstr(funcName, "handle")  || 
		strstr(funcName, "tran")  || 
		strstr(funcName, "uri")  || 
		strstr(funcName, "pod_check")  || 
		strstr(funcName, "accept")  ||
		strstr(funcName, "select")  || 
		strstr(funcName, "boot")  || 
		strstr(funcName, "sleep")  || 
		strstr(funcName, "wait")  || 
		strstr(funcName, "sig")  || 
		strstr(funcName, "server")  || 
		strstr(funcName, "_thread")  || 
		strstr(funcName, "thread_create")  || 
		strstr(funcName, "srv")  || 
		strstr(funcName, "clean")  || 
		strstr(funcName, "acl")  || 
		strstr(funcName, "send_error")  || 
		strstr(funcName, "rollback")  || 
		strstr(funcName, "send_error")  || 
		strstr(funcName, "plugin")  || 
		strstr(funcName, "option")  || 
		strstr(funcName, "var")  || 
		strstr(funcName, "table")  || 
		strstr(funcName, "network")  || 
		strstr(funcName, "thr")  || 
		strstr(funcName, "connection")  || 
		strstr(funcName, "slave")  || 
		strstr(funcName, "execute")  || 
		strstr(funcName, "master")  || 
		strstr(funcName, "sql")  ||
		strstr(funcName, "create") */
		) {
            fprintf(stderr, "Tid %d MYTID %d, executeCall %s\n", gettid(), memoizer->ternMyTid(gettid()), funcName);fflush(stderr);
            	//ki->inst->getParent()->getParent()->getNameStr().c_str(),
            	//ki->inst->getParent()->getNameStr().c_str());
              //fprintf(stderr, "queue: %s\n", memoizer->getQueue()->PrintTids().c_str());fflush(stderr);	
  	}

	if (strstr(funcName, START_TASK_LANDMARK) || strstr(funcName, END_TASK_LANDMARK)) {
		int inst_id = exeInstIDs[(long)(state.prevPC->inst)];
		/*fprintf(stderr, "enter landmark %s, state.stateInWindow %d, state pid %d, tid %d, mytid %d\n", 
					funcName.c_str(), state.stateInWindow, state.pid, gettid(), memoizer->getQueue()->getTidMap());
		fflush(stderr);*/
		if (strstr(funcName, START_TASK_LANDMARK)) {
			assert(state.stateInWindow == 0);
			// Heming: first tries to get into the window, and then check the constraints (including myself). This is correct.
			memoizer->taskStart(&(state.threadLocalWindowSerialNum), inst_id, 0, NULL, 0, NULL);
			/*fprintf(stderr, "start landmark %s, state.stateInWindow %d, state pid %d, tid %d, mytid %d\n", 
					funcName.c_str(), state.stateInWindow, state.pid, gettid(), memoizer->getQueue()->getTidMap());
			fflush(stderr);*/
			state.stateInWindow = 1;
			//appendTidToSCache(state);
		} else {
			if (state.stateInWindow != 1) {
				/*fprintf(stderr, "end landmark %s, state.stateInWindow %d, state pid %d, tid %d, mytid %d\n", 
					funcName.c_str(), state.stateInWindow, state.pid, gettid(), memoizer->getQueue()->getTidMap());
				fflush(stderr);*/
				assert(false);
			}
			state.stateInWindow = 0;

			// This is for a per-task finish. For each task that has been finished, conretize the state.
			//appendTaskToSCache(state);
			concretizeState(state);
			memoizer->taskEnd(&(state.threadLocalWindowSerialNum), inst_id, 0);
		}
	}

  // Should pass arguments, not concrete arguments.
  if (fastExecutionForMemOps(funcName, state, ki, f, arguments))
    return;

  Instruction *i = ki->inst;
  if (f && f->isDeclaration()) {
    switch(f->getIntrinsicID()) {
    case Intrinsic::not_intrinsic:
      // state may be destroyed by this call, cannot touch
      callExternalFunction(state, ki, f, concrete_arguments);
      break;
        
      // va_arg is handled by caller and intrinsic lowering, see comment for
      // ExecutionState::varargs
    case Intrinsic::vastart:  {
      StackFrame &sf = state.stack.back();
      assert(sf.varargs && 
             "vastart called in function with no vararg object");

      // FIXME: This is really specific to the architecture, not the pointer
      // size. This happens to work fir x86-32 and x86-64, however.
      Expr::Width WordSize = Context::get().getPointerWidth();
      if (WordSize == Expr::Int32) {
        executeMemoryOperation(state, true, arguments[0], 
                               sf.varargs->getBaseExpr(), 0);
      } else {
        assert(WordSize == Expr::Int64 && "Unknown word size!");

        // X86-64 has quite complicated calling convention. However,
        // instead of implementing it, we can do a simple hack: just
        // make a function believe that all varargs are on stack.
        executeMemoryOperation(state, true, arguments[0],
                               ConstantExpr::create(48, 32), 0); // gp_offset
        executeMemoryOperation(state, true,
                               AddExpr::create(arguments[0], 
                                               ConstantExpr::create(4, 64)),
                               ConstantExpr::create(304, 32), 0); // fp_offset
        executeMemoryOperation(state, true,
                               AddExpr::create(arguments[0], 
                                               ConstantExpr::create(8, 64)),
                               sf.varargs->getBaseExpr(), 0); // overflow_arg_area
        executeMemoryOperation(state, true,
                               AddExpr::create(arguments[0], 
                                               ConstantExpr::create(16, 64)),
                               ConstantExpr::create(0, 64), 0); // reg_save_area
      }
      break;
    }
    case Intrinsic::vaend:
      // va_end is a noop for the interpreter.
      //
      // FIXME: We should validate that the target didn't do something bad
      // with vaeend, however (like call it twice).
      break;
        
    case Intrinsic::vacopy:
      // va_copy should have been lowered.
      //
      // FIXME: It would be nice to check for errors in the usage of this as
      // well.
    default:
      klee_error("unknown intrinsic: %s", f->getName().data());
    }

    if (InvokeInst *ii = dyn_cast<InvokeInst>(i))
      transferToBasicBlock(ii->getNormalDest(), i->getParent(), state);
  } else {
    //fprintf(stderr, "KLEE::Executor function %s is not declaration\n", funcName);
    // FIXME: I'm not really happy about this reliance on prevPC but it is ok, I
    // guess. This just done to avoid having to pass KInstIterator everywhere
    // instead of the actual instruction, since we can't make a KInstIterator
    // from just an instruction (unlike LLVM).
    KFunction *kf = kmodule->functionMap[f];
    state.pushFrame(state.prevPC, kf);
    state.pc = kf->instructions;

/*        
    if (statsTracker)
      statsTracker->framePushed(state, &state.stack[state.stack.size()-2]);
*/
 
     // TODO: support "byval" parameter attribute
     // TODO: support zeroext, signext, sret attributes
        
    unsigned callingArgs = arguments.size();
    unsigned funcArgs = f->arg_size();
    if (!f->isVarArg()) {
      if (callingArgs > funcArgs) {
        klee_warning_once(f, "calling %s with extra arguments.", 
                          f->getName().data());
      } else if (callingArgs < funcArgs) {
        terminateStateOnError(state, "calling function with too few arguments", 
                              "user.err");
        return;
      }
    } else {
      if (callingArgs < funcArgs) {
        terminateStateOnError(state, "calling function with too few arguments", 
                              "user.err");
        return;
      }
            
      StackFrame &sf = state.stack.back();
      unsigned size = 0;
      for (unsigned i = funcArgs; i < callingArgs; i++) {
        // FIXME: This is really specific to the architecture, not the pointer
        // size. This happens to work fir x86-32 and x86-64, however.
        Expr::Width WordSize = Context::get().getPointerWidth();
        if (WordSize == Expr::Int32) {
          size += Expr::getMinBytesForWidth(arguments[i]->getWidth());
        } else {
          size += llvm::RoundUpToAlignment(arguments[i]->getWidth(), 
                                           WordSize) / 8;
        }
      }

      MemoryObject *mo = sf.varargs = memory->allocate(size, true, false, 
                                                       state.prevPC->inst);
      if (!mo) {
        terminateStateOnExecError(state, "out of memory (varargs)");
        return;
      }
      ObjectState *os = bindObjectInState(state, mo, true);
      unsigned offset = 0;
      for (unsigned i = funcArgs; i < callingArgs; i++) {
        // FIXME: This is really specific to the architecture, not the pointer
        // size. This happens to work fir x86-32 and x86-64, however.
        Expr::Width WordSize = Context::get().getPointerWidth();
        if (WordSize == Expr::Int32) {
          os->write(offset, arguments[i]);
          os->writeConcrete(offset, concrete_arguments[i]);
          offset += Expr::getMinBytesForWidth(arguments[i]->getWidth());
        } else {
          assert(WordSize == Expr::Int64 && "Unknown word size!");
          os->write(offset, arguments[i]);
          os->writeConcrete(offset, concrete_arguments[i]);
          offset += llvm::RoundUpToAlignment(arguments[i]->getWidth(), 
                                             WordSize) / 8;
        }
      }
    }

    unsigned numFormals = f->arg_size();
    for (unsigned i=0; i<numFormals; ++i) {
      bindArgument(kf, i, state, arguments[i]);
      bindArgumentConcrete(kf, i, state, concrete_arguments[i]);

      //Xiaowei
      //writeShdwReg(kf, i, state,te);
    }
  }
}

void Executor::transferToBasicBlock(BasicBlock *dst, BasicBlock *src, 
                                    ExecutionState &state) {
  // Note that in general phi nodes can reuse phi values from the same
  // block but the incoming value is the eval() result *before* the
  // execution of any phi nodes. this is pathological and doesn't
  // really seem to occur, but just in case we run the PhiCleanerPass
  // which makes sure this cannot happen and so it is safe to just
  // eval things in order. The PhiCleanerPass also makes sure that all
  // incoming blocks have the same order for each PHINode so we only
  // have to compute the index once.
  //
  // With that done we simply set an index in the state so that PHI
  // instructions know which argument to eval, set the pc, and continue.
  
  // XXX this lookup has to go ?
  KFunction *kf = state.stack.back().kf;
  unsigned entry = kf->basicBlockEntry[dst];
  state.pc = &kf->instructions[entry];
  if (state.pc->inst->getOpcode() == Instruction::PHI) {
    PHINode *first = static_cast<PHINode*>(state.pc->inst);
    state.incomingBBIndex = first->getBasicBlockIndex(src);
  }
}

void Executor::printFileLine(ExecutionState &state, KInstruction *ki) {
  const InstructionInfo &ii = *ki->info;
  if (ii.file != "") 
    std::cerr << "     " << ii.file << ":" << ii.line << ":";
  else
    std::cerr << "     [no debug info]:";
}


Function* Executor::getCalledFunction(CallSite &cs, ExecutionState &state) {
  Function *f = cs.getCalledFunction();
  
  if (f) {
    std::string alias = state.getFnAlias(f->getName());
    if (alias != "") {
      llvm::Module* currModule = kmodule->module;
      Function* old_f = f;
      f = currModule->getFunction(alias);
      if (!f) {
	llvm::errs() << "Function " << alias << "(), alias for " 
                     << old_f->getName() << " not found!\n";
	assert(f && "function alias not found");
      }
    }
  }
  
  return f;
}

static bool isDebugIntrinsic(const Function *f, KModule *KM) {
#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 7)
  // Fast path, getIntrinsicID is slow.
  if (f == KM->dbgStopPointFn)
    return true;

  switch (f->getIntrinsicID()) {
  case Intrinsic::dbg_stoppoint:
  case Intrinsic::dbg_region_start:
  case Intrinsic::dbg_region_end:
  case Intrinsic::dbg_func_start:
  case Intrinsic::dbg_declare:
    return true;

  default:
    return false;
  }
#else
  return false;
#endif
}

static inline const llvm::fltSemantics * fpWidthToSemantics(unsigned width) {
  switch(width) {
  case Expr::Int32:
    return &llvm::APFloat::IEEEsingle;
  case Expr::Int64:
    return &llvm::APFloat::IEEEdouble;
  case Expr::Fl80:
    return &llvm::APFloat::x87DoubleExtended;
  default:
    return 0;
  }
}

void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
  Instruction *i = ki->inst;
  //Xiaowei
  long instance = slicer->addKinsToDB(ki); //update ins db
  TraceEntry * tentry = new TraceEntry();
  tentry->kins = ki;
  tentry->kfun = state.stack.back().kf;
  tentry->instance = instance;
  tentry->pid = gettid();
  tentry->id = slicer->getCount();
  tentry->caller = NULL;
  ki->te = tentry;

  state.cur_te = tentry;
  slicer->set_cur_te(tentry);

  slicer->addToTrace(tentry);
  slicer->incCount();

  //llvm::errs()  << *i << "\n";
  //llvm::errs()  << *i << "\n";
  //Xiaowei end

  switch (i->getOpcode()) {
    // Control flow
  case Instruction::Ret: {
    ReturnInst *ri = cast<ReturnInst>(i);
    KInstIterator kcaller = state.stack.back().caller;
    Instruction *caller = kcaller ? kcaller->inst : 0;
    bool isVoidReturn = (ri->getNumOperands() == 0);
    ref<Expr> result = ConstantExpr::alloc(0, Expr::Bool);
    ref<Expr> concrete_result = ConstantExpr::alloc(0, Expr::Bool);
    
    //Xiaowei
    if ( kcaller) {
    	tentry->caller = kcaller->te;
    }

    if (!isVoidReturn) {
      result = eval(ki, 0, state).value;
      concrete_result = eval(ki, 0, state).concrete_value;

      //Xiaowei
      addEdge(ki, 0, state, tentry);
    }
    
    if (state.stack.size() <= 1) {
      assert(!caller && "caller set on initial stack frame");
      terminateStateOnExit(state, 0);
    } else {
      state.popFrame();
/*
      if (statsTracker)
        statsTracker->framePopped(state);
*/
      if (InvokeInst *ii = dyn_cast<InvokeInst>(caller)) {
        transferToBasicBlock(ii->getNormalDest(), caller->getParent(), state);
      } else {
        state.pc = kcaller;
        ++state.pc;
      }

      if (!isVoidReturn) {
        const Type *t = caller->getType();
        if (t != Type::getVoidTy(getGlobalContext())) {
          // may need to do coercion due to bitcasts
          Expr::Width from = result->getWidth();
          Expr::Width to = getWidthForLLVMType(t);
            
          if (from != to) {
            CallSite cs = (isa<InvokeInst>(caller) ? CallSite(cast<InvokeInst>(caller)) : 
                           CallSite(cast<CallInst>(caller)));

            // XXX need to check other param attrs ?
            if (cs.paramHasAttr(0, llvm::Attribute::SExt)) {
              result = SExtExpr::create(result, to);
              concrete_result = SExtExpr::create(concrete_result, to);
            } else {
              result = ZExtExpr::create(result, to);
              concrete_result = ZExtExpr::create(concrete_result, to);
            }
          }

          bindLocal(kcaller, state, result);
          bindLocalConcrete(kcaller, state, concrete_result);

          //Xiaowei
          //writeShdwReg(kcaller, state,tentry);
        }
      } else {
        // We check that the return value has no users instead of
        // checking the type, since C defaults to returning int for
        // undeclared functions.
        if (!caller->use_empty()) {
          terminateStateOnExecError(state, "return void when caller expected a result");
        }
      }
    }
    tentry->destvalue = result;
    tentry->operandsvalues.push_back(result);
    tentry->operandsvalues_concrete.push_back(concrete_result);
    tentry->destvalue_concrete = concrete_result;
    tentry->ret_addr = state.stack.back().caller;
    break;
  }
  case Instruction::Unwind: {
    for (;;) {
      KInstruction *kcaller = state.stack.back().caller;
      state.popFrame();
/*
      if (statsTracker)
        statsTracker->framePopped(state);
*/
      if (state.stack.empty()) {
        terminateStateOnExecError(state, "unwind from initial stack frame");
        break;
      } else {
        Instruction *caller = kcaller->inst;
        if (InvokeInst *ii = dyn_cast<InvokeInst>(caller)) {

          //Xiaowei
          tentry->ret_addr = kcaller;

          transferToBasicBlock(ii->getUnwindDest(), caller->getParent(), state);
          break;
        }
      }
    }
    break;
  }
  case Instruction::Br: {
    BranchInst *bi = cast<BranchInst>(i);
    if (bi->isUnconditional()) {
      transferToBasicBlock(bi->getSuccessor(0), bi->getParent(), state);
    } else {
      // FIXME: Find a way that we don't have this hidden dependency.
      assert(bi->getCondition() == bi->getOperand(0) &&
             "Wrong operand index!");
      ref<Expr> cond = eval(ki, 0, state).value;
      //Executor::StatePair branches = fork(state, cond, false);
      // Heming
      ref<Expr> concrete_cond = eval(ki, 0, state).concrete_value;

      //Xiaowei
      addEdge(ki, 0, state, tentry);
      tentry->operandsvalues.push_back(cond);
      tentry->operandsvalues_concrete.push_back(concrete_cond);
      //Xiaowei

      Executor::StatePair branches = fork(state, cond, false, &concrete_cond);

      // NOTE: There is a hidden dependency here, markBranchVisited
      // requires that we still be in the context of the branch
      // instruction (it reuses its statistic id). Should be cleaned
      // up with convenient instruction specific data.
/*      if (statsTracker && state.stack.back().kf->trackCoverage)
        statsTracker->markBranchVisited(branches.first, branches.second);*/

      //Xiaowei Why??
      if (branches.first)
        transferToBasicBlock(bi->getSuccessor(0), bi->getParent(), *branches.first);
      if (branches.second)
        transferToBasicBlock(bi->getSuccessor(1), bi->getParent(), *branches.second);
    }
    break;
  }
  case Instruction::Switch: {
    SwitchInst *si = cast<SwitchInst>(i);
    ref<Expr> cond = eval(ki, 0, state).value;
    unsigned cases = si->getNumCases();
    BasicBlock *bb = si->getParent();


    //Xiaowei
    addEdge(ki, 0, state, tentry);
    tentry->operandsvalues.push_back(cond);
    tentry->operandsvalues_concrete.push_back(eval(ki, 0, state).concrete_value);


    //Heming comment this.
    //cond = toUnique(state, cond);
    // Heming concretize.
    /*if (!isa<ConstantExpr>(cond)) {
	  fprintf(stderr, "concretize swith cond:\n\n");
      cond->print(std::cerr);
	  fprintf(stderr, "\n\n-----------------\n\n");
	  cond = eval(ki, 0, state).concrete_value;
	  cond->print(std::cerr);
	  fprintf(stderr, "\n\nconcretize swith cond end.\n\n");
    }*/

    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(cond)) {
      // Somewhat gross to create these all the time, but fine till we
      // switch to an internal rep.
      const llvm::IntegerType *Ty = 
        cast<IntegerType>(si->getCondition()->getType());
      ConstantInt *ci = ConstantInt::get(Ty, CE->getZExtValue());
      unsigned index = si->findCaseValue(ci);
      transferToBasicBlock(si->getSuccessor(index), si->getParent(), state);
    } else {
      // Heming handles switch, do not need to explore each branch, only explore the first matched branch.
      // There may be a problem if the switch is written like this:
      //case 1:
      //case 2:
      	// do something;
      	
      std::map<BasicBlock*, ref<Expr> > targets;
      ref<Expr> isDefault = ConstantExpr::alloc(1, Expr::Bool);
      bool findBranch = false;
      unsigned ii = 0;
	  for (ii=1; ii<cases; ++ii) {
        ref<Expr> value = evalConstant(si->getCaseValue(ii));
        ref<Expr> concreteCond = eval(ki, 0, state).concrete_value;
        assert(isa<ConstantExpr>(value) && isa<ConstantExpr>(concreteCond));
        if (cast<ConstantExpr>(value)->getZExtValue() == cast<ConstantExpr>(concreteCond)->getZExtValue()) {
          findBranch = true;
		 break;
        }
      }

	  if (findBranch) {
	    // Add constraint, and goto the first matched branch;
	    addConstraint(state, EqExpr::create(cond, eval(ki, 0, state).concrete_value));
        transferToBasicBlock(si->getSuccessor(ii), bb, state);
	  } else {
	    // go to the default branch;
        transferToBasicBlock(si->getSuccessor(0), bb, state);
	  }
   }

    /*{
      std::map<BasicBlock*, ref<Expr> > targets;
      ref<Expr> isDefault = ConstantExpr::alloc(1, Expr::Bool);
      for (unsigned i=1; i<cases; ++i) {
        ref<Expr> value = evalConstant(si->getCaseValue(i));
        ref<Expr> match = EqExpr::create(cond, value);
        isDefault = AndExpr::create(isDefault, Expr::createIsZero(match));
        bool result;
        bool success = solver->mayBeTrue(state, match, result);
        assert(success && "FIXME: Unhandled solver failure");
        (void) success;
        if (result) {
          std::map<BasicBlock*, ref<Expr> >::iterator it =
            targets.insert(std::make_pair(si->getSuccessor(i),
                                          ConstantExpr::alloc(0, Expr::Bool))).first;
          it->second = OrExpr::create(match, it->second);
        }
      }
      bool res;
      bool success = solver->mayBeTrue(state, isDefault, res);
      assert(success && "FIXME: Unhandled solver failure");
      (void) success;
      if (res)
        targets.insert(std::make_pair(si->getSuccessor(0), isDefault));
      
      std::vector< ref<Expr> > conditions;
      for (std::map<BasicBlock*, ref<Expr> >::iterator it = 
             targets.begin(), ie = targets.end();
           it != ie; ++it)
        conditions.push_back(it->second);
      
      std::vector<ExecutionState*> branches;
      branch(state, conditions, branches);
        
      std::vector<ExecutionState*>::iterator bit = branches.begin();
      for (std::map<BasicBlock*, ref<Expr> >::iterator it = 
             targets.begin(), ie = targets.end();
           it != ie; ++it) {
        ExecutionState *es = *bit;
        if (es)
          transferToBasicBlock(it->first, bb, *es);
        ++bit;
      }
    }*/
    break;
 }
  case Instruction::Unreachable:
    // Note that this is not necessarily an internal bug, llvm will
    // generate unreachable instructions in cases where it knows the
    // program will crash. So it is effectively a SEGV or internal
    // error.
    terminateStateOnExecError(state, "reached \"unreachable\" instruction");
    break;

  case Instruction::Invoke:
  case Instruction::Call: { //Xiaowei not yet
    CallSite cs;
    unsigned argStart;
    if (i->getOpcode()==Instruction::Call) {
      cs = CallSite(cast<CallInst>(i));
      argStart = 1;
    } else {
      cs = CallSite(cast<InvokeInst>(i));
      argStart = 3;
    }

    unsigned numArgs = cs.arg_size();
    Function *f = getCalledFunction(cs, state);

    // Skip debug intrinsics, we can't evaluate their metadata arguments.
    if (f && isDebugIntrinsic(f, kmodule))
      break;

    if (state.subRoutine == ki) {
#ifdef MEMOIZER_ORDER
      memoizer->threadCreateEnd(0, 0);
#endif
      /*fprintf(stderr, "Child %d posts Parent %d, MYTID %d, PTHREAD_SELF(%x)\n", 
      	gettid(), getpid(), memoizer->ternMyTid(gettid()), (int)pthread_self());*/
      state.subRoutine = NULL;
      state.threadStopInst = state.pc;
      pthread_create_running = 0;
      executor_print("Child %d posts Parent %d after\n", gettid(), getpid());
    }

    // evaluate arguments
    std::vector< ref<Expr> > arguments;
    arguments.reserve(numArgs);
    std::vector< ref<Expr> > concrete_arguments;
    concrete_arguments.reserve(numArgs);

    for (unsigned j=0; j<numArgs; ++j) {
      arguments.push_back(eval(ki, argStart+j, state).value);
      concrete_arguments.push_back(eval(ki, argStart+j, state).concrete_value);
      //Xiaowei
      addEdge(ki, argStart+j, state, tentry);
      tentry->operandsvalues.push_back(eval(ki, argStart+j, state).value);
      tentry->operandsvalues_concrete.push_back(eval(ki, argStart+j, state).concrete_value);
    }

    if (!f) {
      // special case the call with a bitcast case
      Value *fp = cs.getCalledValue();
      llvm::ConstantExpr *ce = dyn_cast<llvm::ConstantExpr>(fp);
        
      if (ce && ce->getOpcode()==Instruction::BitCast) {
        f = dyn_cast<Function>(ce->getOperand(0));
        assert(f && "XXX unrecognized constant expression in call");
        const FunctionType *fType = 
          dyn_cast<FunctionType>(cast<PointerType>(f->getType())->getElementType());
        const FunctionType *ceType =
          dyn_cast<FunctionType>(cast<PointerType>(ce->getType())->getElementType());
        assert(fType && ceType && "unable to get function type");

        // XXX check result coercion

        // XXX this really needs thought and validation
        unsigned i=0;
        for (std::vector< ref<Expr> >::iterator
               ai = arguments.begin(), ie = arguments.end();
             ai != ie; ++ai) {
          Expr::Width to, from = (*ai)->getWidth();
            
          if (i<fType->getNumParams()) {
            to = getWidthForLLVMType(fType->getParamType(i));

            if (from != to) {
              // XXX need to check other param attrs ?
              if (cs.paramHasAttr(i+1, llvm::Attribute::SExt)) {
                arguments[i] = SExtExpr::create(arguments[i], to);
                concrete_arguments[i] = SExtExpr::create(concrete_arguments[i], to);
              } else {
                arguments[i] = ZExtExpr::create(arguments[i], to);
                concrete_arguments[i] = ZExtExpr::create(concrete_arguments[i], to);
              }
              //Xiaowei
              tentry->operandsvalues[i] = arguments[i];
              tentry->operandsvalues_concrete[i]=concrete_arguments[i];

            }
          }
            
          i++;
        }
      } else if (isa<InlineAsm>(fp)) {
        terminateStateOnExecError(state, "inline assembly is unsupported");
        break;
      }
    }

    if (f) {
      executeCall(state, ki, f, arguments, concrete_arguments, tentry);
    } else {
      ref<Expr> v = eval(ki, 0, state).value;

      ExecutionState *free = &state;
      bool hasInvalid = false, first = true;

      /* XXX This is wasteful, no need to do a full evaluate since we
         have already got a value. But in the end the caches should
         handle it for us, albeit with some overhead. */
      do {
        ref<ConstantExpr> value;
        bool success = solver->getValue(*free, v, value);
        assert(success && "FIXME: Unhandled solver failure");
        (void) success;
        StatePair res = fork(*free, EqExpr::create(v, value), true);
        if (res.first) {
          uint64_t addr = value->getZExtValue();
          if (legalFunctions.count(addr)) {
            f = (Function*) addr;

            // Don't give warning on unique resolution
            if (res.second || !first)
              klee_warning_once((void*) (unsigned long) addr, 
                                "resolved symbolic function pointer to: %s",
                                f->getName().data());

            executeCall(*res.first, ki, f, arguments, concrete_arguments, tentry);
          } else {
            if (!hasInvalid) {
              terminateStateOnExecError(state, "invalid function pointer");
              hasInvalid = true;
            }
          }
        }

        first = false;
        free = res.second;
      } while (free);
    }
    break;
  }
  case Instruction::PHI: { //Xiaowei not yet
    ref<Expr> result = eval(ki, state.incomingBBIndex * 2, state).value;
    bindLocal(ki, state, result);

    if (!isa<ConstantExpr>(eval(ki, state.incomingBBIndex * 2, state).value)) {
      executor_print("WARN: TERN concretize PHI\n");
      result = eval(ki, state.incomingBBIndex * 2, state).concrete_value;
      bindLocalConcrete(ki, state, result);
    }

    break;
  }

    // Special instructions
  case Instruction::Select: {
    SelectInst *SI = cast<SelectInst>(ki->inst);
    assert(SI->getCondition() == SI->getOperand(0) &&
           "Wrong operand index!");
    ref<Expr> cond = eval(ki, 0, state).value;
    ref<Expr> tExpr = eval(ki, 1, state).value;
    ref<Expr> fExpr = eval(ki, 2, state).value;
    ref<Expr> result = SelectExpr::create(cond, tExpr, fExpr);
    bindLocal(ki, state, result);

    //Xiaowei
    addEdge(ki, 0, state, tentry);
    addEdge(ki, 1, state, tentry);
    addEdge(ki, 2, state, tentry);

    //writeShdwReg(ki, state, tentry);

    tentry->operandsvalues.push_back(cond);
    tentry->operandsvalues.push_back(tExpr);
    tentry->operandsvalues.push_back(fExpr);
    tentry->destvalue = result;

    if (!isa<ConstantExpr>(cond) || !isa<ConstantExpr>(tExpr) || !isa<ConstantExpr>(fExpr)) {
      //fprintf(stderr, "WARN: TERN concretize Select\n");
      ref<Expr> cond = eval(ki, 0, state).concrete_value;
      ref<Expr> tExpr = eval(ki, 1, state).concrete_value;
      ref<Expr> fExpr = eval(ki, 2, state).concrete_value;
      ref<Expr> result = SelectExpr::create(cond, tExpr, fExpr);
      bindLocalConcrete(ki, state, result);

      //Xiaowei
      tentry->operandsvalues_concrete.push_back(cond);
      tentry->operandsvalues_concrete.push_back(tExpr);
      tentry->operandsvalues_concrete.push_back(fExpr);
      tentry->destvalue_concrete = result;
    }

    break;
  }

  case Instruction::VAArg: //Xiaowei don't need to handle
    terminateStateOnExecError(state, "unexpected VAArg instruction");
    break;

    // Arithmetic / logical

  case Instruction::Add: {
    ref<Expr> left = eval(ki, 0, state).value;
    ref<Expr> right = eval(ki, 1, state).value;
    bindLocal(ki, state, tentry->destvalue = AddExpr::create(left, right));

    addEdge(ki, 0, state, tentry);
    addEdge(ki, 1, state, tentry);
    //writeShdwReg(ki, state, tentry);
    tentry->operandsvalues.push_back(left);
    tentry->operandsvalues.push_back(right);


    if (!isa<ConstantExpr>(left) || !isa<ConstantExpr>(right)) {
      left = eval(ki, 0, state).concrete_value;
      right = eval(ki, 1, state).concrete_value;
      bindLocalConcrete(ki, state, tentry->destvalue_concrete = AddExpr::create(left, right));

      tentry->operandsvalues_concrete.push_back(left);
      tentry->operandsvalues_concrete.push_back(right);
    }

    break;
  }

  case Instruction::Sub: {
    ref<Expr> left = eval(ki, 0, state).value;
    ref<Expr> right = eval(ki, 1, state).value;
    bindLocal(ki, state, tentry->destvalue = SubExpr::create(left, right));

    //Xiaowei
    addEdge(ki, 0, state, tentry);
    addEdge(ki, 1, state, tentry);
    //writeShdwReg(ki, state, tentry);
    tentry->operandsvalues.push_back(left);
    tentry->operandsvalues.push_back(right);

    if (!isa<ConstantExpr>(left) || !isa<ConstantExpr>(right)) {
      left = eval(ki, 0, state).concrete_value;
      right = eval(ki, 1, state).concrete_value;
      bindLocalConcrete(ki, state, tentry->destvalue_concrete = SubExpr::create(left, right));

      tentry->operandsvalues_concrete.push_back(left);
      tentry->operandsvalues_concrete.push_back(right);
    }

    break;
  }
 
  case Instruction::Mul: {
    ref<Expr> left = eval(ki, 0, state).value;
    ref<Expr> right = eval(ki, 1, state).value;
    bindLocal(ki, state, tentry->destvalue = MulExpr::create(left, right));

    //Xiaowei
    addEdge(ki, 0, state, tentry);
    addEdge(ki, 1, state, tentry);
    //writeShdwReg(ki, state, tentry);
    tentry->operandsvalues.push_back(left);
    tentry->operandsvalues.push_back(right);

    if (!isa<ConstantExpr>(left) || !isa<ConstantExpr>(right)) {
      left = eval(ki, 0, state).concrete_value;
      right = eval(ki, 1, state).concrete_value;
      bindLocalConcrete(ki, state, tentry->destvalue_concrete = MulExpr::create(left, right));

      tentry->operandsvalues_concrete.push_back(left);
      tentry->operandsvalues_concrete.push_back(right);
    }

    break;
  }

  case Instruction::UDiv: {
    ref<Expr> left = eval(ki, 0, state).value;
    ref<Expr> right = eval(ki, 1, state).value;
    ref<Expr> result = UDivExpr::create(left, right);
    bindLocal(ki, state, result);

    //Xiaowei
    addEdge(ki, 0, state, tentry);
    addEdge(ki, 1, state, tentry);
    //writeShdwReg(ki, state, tentry);
    tentry->operandsvalues.push_back(left);
    tentry->operandsvalues.push_back(right);
    tentry->destvalue = result;

    if (!isa<ConstantExpr>(left) || !isa<ConstantExpr>(right)) {
      left = eval(ki, 0, state).concrete_value;
      right = eval(ki, 1, state).concrete_value;
      bindLocalConcrete(ki, state, tentry->destvalue_concrete = UDivExpr::create(left, right));

      tentry->operandsvalues_concrete.push_back(left);
      tentry->operandsvalues_concrete.push_back(right);
    }

    break;
  }

  case Instruction::SDiv: {
    ref<Expr> left = eval(ki, 0, state).value;
    ref<Expr> right = eval(ki, 1, state).value;
    ref<Expr> result = SDivExpr::create(left, right);
    bindLocal(ki, state, result);


    //Xiaowei
    addEdge(ki, 0, state, tentry);
    addEdge(ki, 1, state, tentry);
    //writeShdwReg(ki, state, tentry);
    tentry->operandsvalues.push_back(left);
    tentry->operandsvalues.push_back(right);
    tentry->destvalue = result;

    if (!isa<ConstantExpr>(left) || !isa<ConstantExpr>(right)) {
      left = eval(ki, 0, state).concrete_value;
      right = eval(ki, 1, state).concrete_value;
      bindLocalConcrete(ki, state, tentry->destvalue_concrete = SDivExpr::create(left, right));

      tentry->operandsvalues_concrete.push_back(left);
      tentry->operandsvalues_concrete.push_back(right);
    }

    break;
  }

  case Instruction::URem: {
    ref<Expr> left = eval(ki, 0, state).value;
    ref<Expr> right = eval(ki, 1, state).value;
    ref<Expr> result = URemExpr::create(left, right);
    bindLocal(ki, state, result);

    //Xiaowei
    addEdge(ki, 0, state, tentry);
    addEdge(ki, 1, state, tentry);
    //writeShdwReg(ki, state, tentry);
    tentry->operandsvalues.push_back(left);
    tentry->operandsvalues.push_back(right);
    tentry->destvalue = result;

    if (!isa<ConstantExpr>(left) || !isa<ConstantExpr>(right)) {
      left = eval(ki, 0, state).concrete_value;
      right = eval(ki, 1, state).concrete_value;
      result = URemExpr::create(left, right);
      bindLocalConcrete(ki, state, result);

      tentry->operandsvalues_concrete.push_back(left);
      tentry->operandsvalues_concrete.push_back(right);
      tentry->destvalue_concrete = result;
    }

    break;
  }
 
  case Instruction::SRem: {
    ref<Expr> left = eval(ki, 0, state).value;
    ref<Expr> right = eval(ki, 1, state).value;
    ref<Expr> result = SRemExpr::create(left, right);
    bindLocal(ki, state, result);

    //Xiaowei
    addEdge(ki, 0, state, tentry);
    addEdge(ki, 1, state, tentry);
    //writeShdwReg(ki, state, tentry);
    tentry->operandsvalues.push_back(left);
    tentry->operandsvalues.push_back(right);
    tentry->destvalue = result;

    if (!isa<ConstantExpr>(left) || !isa<ConstantExpr>(right)) {
      left = eval(ki, 0, state).concrete_value;
      right = eval(ki, 1, state).concrete_value;
      result = SRemExpr::create(left, right);
      bindLocalConcrete(ki, state, result);

      tentry->operandsvalues_concrete.push_back(left);
      tentry->operandsvalues_concrete.push_back(right);
      tentry->destvalue_concrete = result;
    }

    break;
  }

  case Instruction::And: {
    ref<Expr> left = eval(ki, 0, state).value;
    ref<Expr> right = eval(ki, 1, state).value;
    ref<Expr> result = AndExpr::create(left, right);
    bindLocal(ki, state, result);

    //Xiaowei
    addEdge(ki, 0, state, tentry);
    addEdge(ki, 1, state, tentry);
    //writeShdwReg(ki, state, tentry);
    tentry->operandsvalues.push_back(left);
    tentry->operandsvalues.push_back(right);
    tentry->destvalue = result;

    if (!isa<ConstantExpr>(left) || !isa<ConstantExpr>(right)) {
      left = eval(ki, 0, state).concrete_value;
      right = eval(ki, 1, state).concrete_value;
      result = AndExpr::create(left, right);
      bindLocalConcrete(ki, state, result);

      tentry->operandsvalues_concrete.push_back(left);
      tentry->operandsvalues_concrete.push_back(right);
      tentry->destvalue_concrete = result;
    }

    break;
  }

  case Instruction::Or: {
    ref<Expr> left = eval(ki, 0, state).value;
    ref<Expr> right = eval(ki, 1, state).value;
    ref<Expr> result = OrExpr::create(left, right);
    bindLocal(ki, state, result);

    //Xiaowei
    addEdge(ki, 0, state, tentry);
    addEdge(ki, 1, state, tentry);
    //writeShdwReg(ki, state, tentry);
    tentry->operandsvalues.push_back(left);
    tentry->operandsvalues.push_back(right);
    tentry->destvalue = result;

    if (!isa<ConstantExpr>(left) || !isa<ConstantExpr>(right)) {
      left = eval(ki, 0, state).concrete_value;
      right = eval(ki, 1, state).concrete_value;
      result = OrExpr::create(left, right);
      bindLocalConcrete(ki, state, result);

      tentry->operandsvalues_concrete.push_back(left);
      tentry->operandsvalues_concrete.push_back(right);
      tentry->destvalue_concrete = result;
    }

    break;
  }

  case Instruction::Xor: {
    ref<Expr> left = eval(ki, 0, state).value;
    ref<Expr> right = eval(ki, 1, state).value;
    ref<Expr> result = XorExpr::create(left, right);
    bindLocal(ki, state, result);

    //Xiaowei
    addEdge(ki, 0, state, tentry);
    addEdge(ki, 1, state, tentry);
    //writeShdwReg(ki, state, tentry);
    tentry->operandsvalues.push_back(left);
    tentry->operandsvalues.push_back(right);
    tentry->destvalue = result;

    if (!isa<ConstantExpr>(left) || !isa<ConstantExpr>(right)) {
      left = eval(ki, 0, state).concrete_value;
      right = eval(ki, 1, state).concrete_value;
      result = XorExpr::create(left, right);
      bindLocalConcrete(ki, state, result);

      tentry->operandsvalues_concrete.push_back(left);
      tentry->operandsvalues_concrete.push_back(right);
      tentry->destvalue_concrete = result;
    }

    break;
  }

  case Instruction::Shl: {
    ref<Expr> left = eval(ki, 0, state).value;
    ref<Expr> right = eval(ki, 1, state).value;
    ref<Expr> result = ShlExpr::create(left, right);
    bindLocal(ki, state, result);

    //Xiaowei
    addEdge(ki, 0, state, tentry);
    addEdge(ki, 1, state, tentry);
    //writeShdwReg(ki, state, tentry);
    tentry->operandsvalues.push_back(left);
    tentry->operandsvalues.push_back(right);
    tentry->destvalue = result;

    if (!isa<ConstantExpr>(left) || !isa<ConstantExpr>(right)) {
      left = eval(ki, 0, state).concrete_value;
      right = eval(ki, 1, state).concrete_value;
      result = ShlExpr::create(left, right);
      bindLocalConcrete(ki, state, result);

      tentry->operandsvalues_concrete.push_back(left);
      tentry->operandsvalues_concrete.push_back(right);
      tentry->destvalue_concrete = result;
    }

    break;
  }

  case Instruction::LShr: {
    ref<Expr> left = eval(ki, 0, state).value;
    ref<Expr> right = eval(ki, 1, state).value;
    ref<Expr> result = LShrExpr::create(left, right);
    bindLocal(ki, state, result);

    //Xiaowei
    addEdge(ki, 0, state, tentry);
    addEdge(ki, 1, state, tentry);
    //writeShdwReg(ki, state, tentry);
    tentry->operandsvalues.push_back(left);
    tentry->operandsvalues.push_back(right);
    tentry->destvalue = result;

    if (!isa<ConstantExpr>(left) || !isa<ConstantExpr>(right)) {
      left = eval(ki, 0, state).concrete_value;
      right = eval(ki, 1, state).concrete_value;
      result = LShrExpr::create(left, right);
      bindLocalConcrete(ki, state, result);

      tentry->operandsvalues_concrete.push_back(left);
      tentry->operandsvalues_concrete.push_back(right);
      tentry->destvalue_concrete = result;
    }

    break;
  }

  case Instruction::AShr: {
    ref<Expr> left = eval(ki, 0, state).value;
    ref<Expr> right = eval(ki, 1, state).value;
    ref<Expr> result = AShrExpr::create(left, right);
    bindLocal(ki, state, result);

    //Xiaowei
    addEdge(ki, 0, state, tentry);
    addEdge(ki, 1, state, tentry);
    //writeShdwReg(ki, state, tentry);
    tentry->operandsvalues.push_back(left);
    tentry->operandsvalues.push_back(right);
    tentry->destvalue = result;

    if (!isa<ConstantExpr>(left) || !isa<ConstantExpr>(right)) {
      left = eval(ki, 0, state).concrete_value;
      right = eval(ki, 1, state).concrete_value;
      result = AShrExpr::create(left, right);
      bindLocalConcrete(ki, state, result);

      tentry->operandsvalues_concrete.push_back(left);
      tentry->operandsvalues_concrete.push_back(right);
      tentry->destvalue_concrete = result;
    }

    break;
  }

    // Compare

  case Instruction::ICmp: {
    CmpInst *ci = cast<CmpInst>(i);
    ICmpInst *ii = cast<ICmpInst>(ci);
 
    switch(ii->getPredicate()) {
    case ICmpInst::ICMP_EQ: {
      ref<Expr> left = eval(ki, 0, state).value;
      ref<Expr> right = eval(ki, 1, state).value;
      ref<Expr> result = EqExpr::create(left, right);
      bindLocal(ki, state, result);

      //Xiaowei
      addEdge(ki, 0, state, tentry);
      addEdge(ki, 1, state, tentry);
      //writeShdwReg(ki, state, tentry);
      tentry->operandsvalues.push_back(left);
      tentry->operandsvalues.push_back(right);
      tentry->destvalue = result;

      if (!isa<ConstantExpr>(left) || !isa<ConstantExpr>(right)) {
        left = eval(ki, 0, state).concrete_value;
        right = eval(ki, 1, state).concrete_value;
        result = EqExpr::create(left, right);
        bindLocalConcrete(ki, state, result);

        tentry->operandsvalues_concrete.push_back(left);
        tentry->operandsvalues_concrete.push_back(right);
        tentry->destvalue_concrete = result;
      }

      break;
    }

    case ICmpInst::ICMP_NE: {
      ref<Expr> left = eval(ki, 0, state).value;
      ref<Expr> right = eval(ki, 1, state).value;
      ref<Expr> result = NeExpr::create(left, right);
      bindLocal(ki, state, result);

      //Xiaowei
      addEdge(ki, 0, state, tentry);
      addEdge(ki, 1, state, tentry);
      //writeShdwReg(ki, state, tentry);
      tentry->operandsvalues.push_back(left);
      tentry->operandsvalues.push_back(right);
      tentry->destvalue = result;

      if (!isa<ConstantExpr>(left) || !isa<ConstantExpr>(right)) {
        left = eval(ki, 0, state).concrete_value;
        right = eval(ki, 1, state).concrete_value;
        result = NeExpr::create(left, right);
        bindLocalConcrete(ki, state, result);

        tentry->operandsvalues_concrete.push_back(left);
        tentry->operandsvalues_concrete.push_back(right);
        tentry->destvalue_concrete = result;
      }

      break;
    }

    case ICmpInst::ICMP_UGT: {
      ref<Expr> left = eval(ki, 0, state).value;
      ref<Expr> right = eval(ki, 1, state).value;
      ref<Expr> result = UgtExpr::create(left, right);
      bindLocal(ki, state,result);

      //Xiaowei
      addEdge(ki, 0, state, tentry);
      addEdge(ki, 1, state, tentry);
      //writeShdwReg(ki, state, tentry);
      tentry->operandsvalues.push_back(left);
      tentry->operandsvalues.push_back(right);
      tentry->destvalue = result;

      if (!isa<ConstantExpr>(left) || !isa<ConstantExpr>(right)) {
        left = eval(ki, 0, state).concrete_value;
        right = eval(ki, 1, state).concrete_value;
        result = UgtExpr::create(left, right);
        bindLocalConcrete(ki, state, result);

        tentry->operandsvalues_concrete.push_back(left);
        tentry->operandsvalues_concrete.push_back(right);
        tentry->destvalue_concrete = result;
      }

      break;
    }

    case ICmpInst::ICMP_UGE: {
      ref<Expr> left = eval(ki, 0, state).value;
      ref<Expr> right = eval(ki, 1, state).value;
      ref<Expr> result = UgeExpr::create(left, right);
      bindLocal(ki, state, result);

      //Xiaowei
      addEdge(ki, 0, state, tentry);
      addEdge(ki, 1, state, tentry);
      //writeShdwReg(ki, state, tentry);
      tentry->operandsvalues.push_back(left);
      tentry->operandsvalues.push_back(right);
      tentry->destvalue = result;

      if (!isa<ConstantExpr>(left) || !isa<ConstantExpr>(right)) {
        left = eval(ki, 0, state).concrete_value;
        right = eval(ki, 1, state).concrete_value;
        result = UgeExpr::create(left, right);
        bindLocalConcrete(ki, state, result);

        tentry->operandsvalues_concrete.push_back(left);
        tentry->operandsvalues_concrete.push_back(right);
        tentry->destvalue_concrete = result;
      }

      break;
    }

    case ICmpInst::ICMP_ULT: {
      ref<Expr> left = eval(ki, 0, state).value;
      ref<Expr> right = eval(ki, 1, state).value;
      ref<Expr> result = UltExpr::create(left, right);
      bindLocal(ki, state, result);

      //Xiaowei
      addEdge(ki, 0, state, tentry);
      addEdge(ki, 1, state, tentry);
      //writeShdwReg(ki, state, tentry);
      tentry->operandsvalues.push_back(left);
      tentry->operandsvalues.push_back(right);
      tentry->destvalue = result;

      if (!isa<ConstantExpr>(left) || !isa<ConstantExpr>(right)) {
        left = eval(ki, 0, state).concrete_value;
        right = eval(ki, 1, state).concrete_value;
        result = UltExpr::create(left, right);
        bindLocalConcrete(ki, state, result);

        tentry->operandsvalues_concrete.push_back(left);
        tentry->operandsvalues_concrete.push_back(right);
        tentry->destvalue_concrete = result;
      }

      break;
    }

    case ICmpInst::ICMP_ULE: {
      ref<Expr> left = eval(ki, 0, state).value;
      ref<Expr> right = eval(ki, 1, state).value;
      ref<Expr> result = UleExpr::create(left, right);
      bindLocal(ki, state, result);

      //Xiaowei
      addEdge(ki, 0, state, tentry);
      addEdge(ki, 1, state, tentry);
      //writeShdwReg(ki, state, tentry);
      tentry->operandsvalues.push_back(left);
      tentry->operandsvalues.push_back(right);
      tentry->destvalue = result;

      if (!isa<ConstantExpr>(left) || !isa<ConstantExpr>(right)) {
        left = eval(ki, 0, state).concrete_value;
        right = eval(ki, 1, state).concrete_value;
        result = UleExpr::create(left, right);
        bindLocalConcrete(ki, state, result);

        tentry->operandsvalues_concrete.push_back(left);
        tentry->operandsvalues_concrete.push_back(right);
        tentry->destvalue_concrete = result;
      }

      break;
    }

    case ICmpInst::ICMP_SGT: {
      ref<Expr> left = eval(ki, 0, state).value;
      ref<Expr> right = eval(ki, 1, state).value;
      ref<Expr> result = SgtExpr::create(left, right);
      bindLocal(ki, state, result);

      //Xiaowei
      addEdge(ki, 0, state, tentry);
      addEdge(ki, 1, state, tentry);
      //writeShdwReg(ki, state, tentry);
      tentry->operandsvalues.push_back(left);
      tentry->operandsvalues.push_back(right);
      tentry->destvalue = result;

      if (!isa<ConstantExpr>(left) || !isa<ConstantExpr>(right)) {
        left = eval(ki, 0, state).concrete_value;
        right = eval(ki, 1, state).concrete_value;
        result = SgtExpr::create(left, right);
        bindLocalConcrete(ki, state, result);

        tentry->operandsvalues_concrete.push_back(left);
        tentry->operandsvalues_concrete.push_back(right);
        tentry->destvalue_concrete = result;
      }

      break;
    }

    case ICmpInst::ICMP_SGE: {
      ref<Expr> left = eval(ki, 0, state).value;
      ref<Expr> right = eval(ki, 1, state).value;
      ref<Expr> result = SgeExpr::create(left, right);
      bindLocal(ki, state, result);

      //Xiaowei
      addEdge(ki, 0, state, tentry);
      addEdge(ki, 1, state, tentry);
      //writeShdwReg(ki, state, tentry);
      tentry->operandsvalues.push_back(left);
      tentry->operandsvalues.push_back(right);
      tentry->destvalue = result;

      if (!isa<ConstantExpr>(left) || !isa<ConstantExpr>(right)) {
        left = eval(ki, 0, state).concrete_value;
        right = eval(ki, 1, state).concrete_value;
        result = SgeExpr::create(left, right);
        bindLocalConcrete(ki, state, result);

        tentry->operandsvalues_concrete.push_back(left);
        tentry->operandsvalues_concrete.push_back(right);
        tentry->destvalue_concrete = result;
      }

      break;
    }

    case ICmpInst::ICMP_SLT: {
      ref<Expr> left = eval(ki, 0, state).value;
      ref<Expr> right = eval(ki, 1, state).value;
      ref<Expr> result = SltExpr::create(left, right);
      bindLocal(ki, state, result);

      //Xiaowei
      addEdge(ki, 0, state, tentry);
      addEdge(ki, 1, state, tentry);
      //writeShdwReg(ki, state, tentry);
      tentry->operandsvalues.push_back(left);
      tentry->operandsvalues.push_back(right);
      tentry->destvalue = result;

      if (!isa<ConstantExpr>(left) || !isa<ConstantExpr>(right)) {
        left = eval(ki, 0, state).concrete_value;
        right = eval(ki, 1, state).concrete_value;
        result = SltExpr::create(left, right);
        bindLocalConcrete(ki, state, result);

        tentry->operandsvalues_concrete.push_back(left);
        tentry->operandsvalues_concrete.push_back(right);
        tentry->destvalue_concrete = result;
      }

      break;
    }

    case ICmpInst::ICMP_SLE: {
      ref<Expr> left = eval(ki, 0, state).value;
      ref<Expr> right = eval(ki, 1, state).value;
      ref<Expr> result = SleExpr::create(left, right);
      bindLocal(ki, state, result);

      //Xiaowei
      addEdge(ki, 0, state, tentry);
      addEdge(ki, 1, state, tentry);
      //writeShdwReg(ki, state, tentry);
      tentry->operandsvalues.push_back(left);
      tentry->operandsvalues.push_back(right);
      tentry->destvalue = result;

      if (!isa<ConstantExpr>(left) || !isa<ConstantExpr>(right)) {
        left = eval(ki, 0, state).concrete_value;
        right = eval(ki, 1, state).concrete_value;
        result = SleExpr::create(left, right);
        bindLocalConcrete(ki, state, result);

        tentry->operandsvalues_concrete.push_back(left);
        tentry->operandsvalues_concrete.push_back(right);
        tentry->destvalue_concrete = result;
      }

      break;
    }

    default:
      terminateStateOnExecError(state, "invalid ICmp predicate");
    }
    break;
  }
 
    // Memory instructions...
#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 7)
  case Instruction::Malloc:
  case Instruction::Alloca: {
    AllocationInst *ai = cast<AllocationInst>(i);
#else
  case Instruction::Alloca: { // Xiaowei not yet
    AllocaInst *ai = cast<AllocaInst>(i);
#endif
    unsigned elementSize = 
      kmodule->targetData->getTypeStoreSize(ai->getAllocatedType());
    ref<Expr> size = Expr::createPointer(elementSize);
    if (ai->isArrayAllocation()) {
      //ref<Expr> count = eval(ki, 0, state).value;

      // Heming: Temporarily method is just handle concrete_value, since we do not need to explore all sizes for malloc, 
      // just like we do not need to explore all pthread_create in a for loop.
      //ref<Expr> count = eval(ki, 0, state).value;
      if (!isa<ConstantExpr>(eval(ki, 0, state).value)) {
        fprintf(stderr, "NOTE: TERN concretize symbolic variable for alloc/malloc operation\n");
      }
      ref<Expr> count = eval(ki, 0, state).concrete_value;

      //Xiaowei
      addEdge(ki, 0, state, tentry);
      tentry->operandsvalues.push_back(eval(ki, 0, state).value);
      tentry->operandsvalues_concrete.push_back(count);


      count = Expr::createCoerceToPointerType(count);
      size = MulExpr::create(size, count);
    }
    bool isLocal = i->getOpcode()==Instruction::Alloca;
    executeAlloc(state, size, isLocal, ki);
    break;
  }
#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 7)
  case Instruction::Free: {
    //executeFree(state, eval(ki, 0, state).value);

		executor_print("Pid %d Instruction::Free\n", getpid());
    //executeFree(state, eval(ki, 0, state).value);
    // Heming: concretize the address.
    //executeFree(state, eval(ki, 0, state).value);
    if (!isa<ConstantExpr>(eval(ki, 0, state).value)) {
      fprintf(stderr, "WARN: TERN concretize for free/delete\n");
    }
    executeFree(state, eval(ki, 0, state).concrete_value);
    break;
  }
#endif

  case Instruction::Load: { //Xiaowei not yet
    // Heming changes this at 2010-3-4.
    ref<Expr> base = eval(ki, 0, state).concrete_value;
    if (!isa<ConstantExpr>(eval(ki, 0, state).value)) {
      executor_print("WARN: TERN concretize addr for load\n");
    }

    //Xiaowei
    addEdge(ki, 0, state, tentry);
    tentry->operandsvalues.push_back(eval(ki, 0, state).value);
    tentry->operandsvalues_concrete.push_back(base);

	//ref<Expr> base = eval(ki, 0, state).value;
    executeMemoryOperation(state, false, base, 0, ki, false);
    break;
  }
  case Instruction::Store: { //Xiaowei not yet
    // Heming changes this at 2010-3-4.
    //ref<Expr> base = eval(ki, 1, state).value;
    ref<Expr> base = eval(ki, 1, state).concrete_value;	
    ref<Expr> value = eval(ki, 0, state).value;

    //Xiaowei

    tentry->operandsvalues.push_back(eval(ki, 1, state).value);
    tentry->operandsvalues.push_back(eval(ki, 0, state).value);
    tentry->operandsvalues_concrete.push_back(base);

    addEdge(ki, 0, state, tentry);
    addEdge(ki, 1, state, tentry);

    if (!isa<ConstantExpr>(eval(ki, 1, state).value)) {
      executor_print("WARN: TERN concretize addr for store\n");
    }
    executeMemoryOperation(state, true, base, value, ki, false);

    // Heming
    if (!isa<ConstantExpr>(value)) {
      executor_print("WARN: TERN concretize value for store\n");
      value = eval(ki, 0, state).concrete_value;
      //Xiaowei
      tentry->operandsvalues_concrete.push_back(value);

      executeMemoryOperation(state, true, base, value, ki, true);
    }
    break;
  }

  case Instruction::GetElementPtr: { //Xiaowei not yet
/*    KGEPInstruction *kgepi = static_cast<KGEPInstruction*>(ki);
    ref<Expr> base = eval(ki, 0, state).value;

    for (std::vector< std::pair<unsigned, uint64_t> >::iterator 
           it = kgepi->indices.begin(), ie = kgepi->indices.end(); 
         it != ie; ++it) {
      uint64_t elementSize = it->second;
      ref<Expr> index = eval(ki, it->first, state).value;
      base = AddExpr::create(base,
                             MulExpr::create(Expr::createCoerceToPointerType(index),
                                             Expr::createPointer(elementSize)));
    }
    if (kgepi->offset)
      base = AddExpr::create(base,
                             Expr::createPointer(kgepi->offset));
    bindLocal(ki, state, base);*/

    executor_print( "Pid %d Instruction::GetElementPtr\n", gettid());
    //std::cerr << "GetElementPtr Inst " << *(ki->inst) << "\n";
    KGEPInstruction *kgepi = static_cast<KGEPInstruction*>(ki);
    ref<Expr> base = eval(ki, 0, state).value;


    //Xiaowei
    addEdge(ki, 0, state, tentry);
    tentry->operandsvalues.push_back(base);


    executor_print( "GetElementPtr index size %u\n", kgepi->indices.size());
    for (std::vector< std::pair<unsigned, uint64_t> >::iterator 
           it = kgepi->indices.begin(), ie = kgepi->indices.end(); 
         it != ie; ++it) {
      uint64_t elementSize = it->second;
      ref<Expr> index = eval(ki, it->first, state).value;

      //Xiaowei
      addEdge(ki, it->first, state, tentry);
      tentry->operandsvalues.push_back(index);

      executor_print( "GetElementPtr index %llu\n", cast<ConstantExpr>(index)->getZExtValue());
      base = AddExpr::create(base,
                             MulExpr::create(Expr::createCoerceToPointerType(index),
                                             Expr::createPointer(elementSize)));
    }
    if (kgepi->offset)
      base = AddExpr::create(base,
                             Expr::createPointer(kgepi->offset));
    bindLocal(ki, state, base);

    tentry->destvalue = base;
    //Xiaowei
    //writeShdwReg(ki, state, tentry);


    // Heming: handle concrete operation.  
    if (!isa<ConstantExpr>(eval(ki, 0, state).value)) {
      executor_print("WARN: TERN concretize addr for getelementptr\n");
    }
    base = eval(ki, 0, state).concrete_value;

    tentry->operandsvalues_concrete.push_back(base);

    //fprintf(stderr, "GetElementPtr index size %u\n", kgepi->indices.size());
    for (std::vector< std::pair<unsigned, uint64_t> >::iterator 
           it = kgepi->indices.begin(), ie = kgepi->indices.end(); 
         it != ie; ++it) {
      uint64_t elementSize = it->second;
      ref<Expr> index = eval(ki, it->first, state).concrete_value;

      tentry->operandsvalues_concrete.push_back(index);

      if (!isa<ConstantExpr>(eval(ki, it->first, state).value)) {
        executor_print("WARN: TERN concretize index for getelementptr\n");
      }
      //fprintf(stderr, "GetElementPtr index %llu\n", cast<ConstantExpr>(index)->getZExtValue());
      base = AddExpr::create(base,
                             MulExpr::create(Expr::createCoerceToPointerType(index),
                                             Expr::createPointer(elementSize)));
    }
    if (kgepi->offset)
      base = AddExpr::create(base,
                             Expr::createPointer(kgepi->offset));
    bindLocalConcrete(ki, state, base);

    tentry->destvalue_concrete = base;

    break;
  }

    // Conversion
  case Instruction::Trunc: {
    CastInst *ci = cast<CastInst>(i);
    ref<Expr> result = ExtractExpr::create(eval(ki, 0, state).value,
                                           0,
                                           getWidthForLLVMType(ci->getType()));
    //Xiaowei
    addEdge(ki, 0, state, tentry);
    tentry->operandsvalues.push_back(eval(ki, 0, state).value);
    tentry->destvalue = result;
    //writeShdwReg(ki, state, tentry);

    bindLocal(ki, state, result);

    if (!isa<ConstantExpr>(result)) {
      result = ExtractExpr::create(eval(ki, 0, state).concrete_value,
                                           0,
                                           getWidthForLLVMType(ci->getType()));
      bindLocalConcrete(ki, state, result);

      tentry->operandsvalues_concrete.push_back(eval(ki, 0, state).concrete_value);
      tentry->destvalue_concrete = result;
    }

    break;
  }
  case Instruction::ZExt: {
    CastInst *ci = cast<CastInst>(i);
    ref<Expr> result = ZExtExpr::create(eval(ki, 0, state).value,
                                        getWidthForLLVMType(ci->getType()));
    bindLocal(ki, state, result);

    //Xiaowei
    addEdge(ki, 0, state, tentry);
    //writeShdwReg(ki, state, tentry);
    tentry->operandsvalues.push_back(eval(ki, 0, state).value);
    tentry->destvalue = result;

    if (!isa<ConstantExpr>(result)) {
      result = ZExtExpr::create(eval(ki, 0, state).concrete_value,
                                        getWidthForLLVMType(ci->getType()));
      bindLocalConcrete(ki, state, result);

      tentry->operandsvalues_concrete.push_back(eval(ki, 0, state).concrete_value);
      tentry->destvalue_concrete = result;
    }

    break;
  }
  case Instruction::SExt: {
    CastInst *ci = cast<CastInst>(i);
    ref<Expr> result = SExtExpr::create(eval(ki, 0, state).value,
                                        getWidthForLLVMType(ci->getType()));
    bindLocal(ki, state, result);

    //Xiaowei
    addEdge(ki, 0, state, tentry);
    //writeShdwReg(ki, state, tentry);
    tentry->operandsvalues.push_back(eval(ki, 0, state).value);
    tentry->destvalue = result;

    if (!isa<ConstantExpr>(result)) {
      result = SExtExpr::create(eval(ki, 0, state).concrete_value,
                                        getWidthForLLVMType(ci->getType()));
      bindLocalConcrete(ki, state, result);

      tentry->operandsvalues_concrete.push_back(eval(ki, 0, state).concrete_value);
      tentry->destvalue_concrete = result;
    }

    break;
  }

  case Instruction::IntToPtr: {
    CastInst *ci = cast<CastInst>(i);
    Expr::Width pType = getWidthForLLVMType(ci->getType());
    ref<Expr> arg = eval(ki, 0, state).value;

    //Xiaowei
    ref<Expr> result = ZExtExpr::create(arg, pType);
    bindLocal(ki, state, result);

    //Xiaowei
    addEdge(ki, 0, state, tentry);
    //writeShdwReg(ki, state, tentry);
    tentry->operandsvalues.push_back(arg);
    tentry->destvalue = result;

    // Heming //Xiaowei
    arg = eval(ki, 0, state).concrete_value;
    bindLocalConcrete(ki, state, tentry->destvalue_concrete = ZExtExpr::create(arg, pType));

    tentry->operandsvalues_concrete.push_back(arg);

    break;
  } 
  case Instruction::PtrToInt: {
    CastInst *ci = cast<CastInst>(i);
    Expr::Width iType = getWidthForLLVMType(ci->getType());
    ref<Expr> arg = eval(ki, 0, state).value;
    //Xiaowei
    ref<Expr> result = ZExtExpr::create(arg, iType);
    bindLocal(ki, state, result);

    //Xiaowei
    addEdge(ki, 0, state, tentry);
    //writeShdwReg(ki, state, tentry);
    tentry->operandsvalues.push_back(arg);
    tentry->destvalue = result;

    // Heming //Xiaowei
    arg = eval(ki, 0, state).concrete_value;
    bindLocalConcrete(ki, state, tentry->destvalue_concrete = ZExtExpr::create(arg, iType));

    tentry->operandsvalues_concrete.push_back(arg);

    break;
  }

  case Instruction::BitCast: {
    ref<Expr> result = eval(ki, 0, state).value;
    bindLocal(ki, state, result);

    //Xiaowei
    tentry->operandsvalues.push_back(eval(ki, 0, state).value);
    tentry->destvalue = result;

    // Heming
    result = eval(ki, 0, state).concrete_value;
    bindLocalConcrete(ki, state, result);

    //Xiaowei
    addEdge(ki, 0, state, tentry);
    //writeShdwReg(ki, state, tentry);
    tentry->operandsvalues_concrete.push_back(eval(ki, 0, state).concrete_value);
    tentry->destvalue_concrete = result;

    break;
  }

    // Floating point instructions
    // Heming: for the floating point instructions below, since KLEE does not support symbolic executions for them,
    // I can simply use their concrete values.
  case Instruction::FAdd: { //Xiaowei not yet
    ref<ConstantExpr> left = toConstant(state, eval(ki, 0, state).concrete_value,
                                        "floating point");
    ref<ConstantExpr> right = toConstant(state, eval(ki, 1, state).concrete_value,
                                         "floating point");
    if (!fpWidthToSemantics(left->getWidth()) ||
        !fpWidthToSemantics(right->getWidth()))
      return terminateStateOnExecError(state, "Unsupported FAdd operation");

    llvm::APFloat Res(left->getAPValue());
    Res.add(APFloat(right->getAPValue()), APFloat::rmNearestTiesToEven);

    //Xiaowei
    addEdge(ki, 0, state, tentry);
    addEdge(ki, 1, state, tentry);


    bindLocal(ki, state,  tentry->destvalue = ConstantExpr::alloc(Res.bitcastToAPInt()));

    //writeShdwReg(ki, state, tentry);
    tentry->operandsvalues.push_back(left);
    tentry->operandsvalues.push_back(right);

    break;
  }

  case Instruction::FSub: {
    ref<ConstantExpr> left = toConstant(state, eval(ki, 0, state).concrete_value,
                                        "floating point");
    ref<ConstantExpr> right = toConstant(state, eval(ki, 1, state).concrete_value,
                                         "floating point");
    if (!fpWidthToSemantics(left->getWidth()) ||
        !fpWidthToSemantics(right->getWidth()))
      return terminateStateOnExecError(state, "Unsupported FSub operation");

    llvm::APFloat Res(left->getAPValue());
    Res.subtract(APFloat(right->getAPValue()), APFloat::rmNearestTiesToEven);
    //Xiaowei
    addEdge(ki, 0, state, tentry);
    addEdge(ki, 1, state, tentry);
    bindLocal(ki, state, tentry->destvalue = ConstantExpr::alloc(Res.bitcastToAPInt()));
    //writeShdwReg(ki, state, tentry);
    tentry->operandsvalues.push_back(left);
    tentry->operandsvalues.push_back(right);
    break;
  }
 
  case Instruction::FMul: {
    ref<ConstantExpr> left = toConstant(state, eval(ki, 0, state).concrete_value,
                                        "floating point");
    ref<ConstantExpr> right = toConstant(state, eval(ki, 1, state).concrete_value,
                                         "floating point");
    if (!fpWidthToSemantics(left->getWidth()) ||
        !fpWidthToSemantics(right->getWidth()))
      return terminateStateOnExecError(state, "Unsupported FMul operation");

    llvm::APFloat Res(left->getAPValue());
    Res.multiply(APFloat(right->getAPValue()), APFloat::rmNearestTiesToEven);

    //Xiaowei
    addEdge(ki, 0, state, tentry);
    addEdge(ki, 1, state, tentry);
    bindLocal(ki, state, tentry->destvalue =  ConstantExpr::alloc(Res.bitcastToAPInt()));
    //writeShdwReg(ki, state, tentry);
    tentry->operandsvalues.push_back(left);
    tentry->operandsvalues.push_back(right);

    break;
  }

  case Instruction::FDiv: {
    ref<ConstantExpr> left = toConstant(state, eval(ki, 0, state).concrete_value,
                                        "floating point");
    ref<ConstantExpr> right = toConstant(state, eval(ki, 1, state).concrete_value,
                                         "floating point");
    if (!fpWidthToSemantics(left->getWidth()) ||
        !fpWidthToSemantics(right->getWidth()))
      return terminateStateOnExecError(state, "Unsupported FDiv operation");

    llvm::APFloat Res(left->getAPValue());
    Res.divide(APFloat(right->getAPValue()), APFloat::rmNearestTiesToEven);
    //Xiaowei
    addEdge(ki, 0, state, tentry);
    addEdge(ki, 1, state, tentry);
    bindLocal(ki, state, tentry->destvalue =  ConstantExpr::alloc(Res.bitcastToAPInt()));
    //writeShdwReg(ki, state, tentry);
    tentry->operandsvalues.push_back(left);
    tentry->operandsvalues.push_back(right);
    break;
  }

  case Instruction::FRem: { // Xiaowei not yet
    ref<ConstantExpr> left = toConstant(state, eval(ki, 0, state).concrete_value,
                                        "floating point");
    ref<ConstantExpr> right = toConstant(state, eval(ki, 1, state).concrete_value,
                                         "floating point");
    if (!fpWidthToSemantics(left->getWidth()) ||
        !fpWidthToSemantics(right->getWidth()))
      return terminateStateOnExecError(state, "Unsupported FRem operation");

    llvm::APFloat Res(left->getAPValue());
    Res.mod(APFloat(right->getAPValue()), APFloat::rmNearestTiesToEven);
    //Xiaowei
    addEdge(ki, 0, state, tentry);
    addEdge(ki, 1, state, tentry);
    bindLocal(ki, state, tentry->destvalue = ConstantExpr::alloc(Res.bitcastToAPInt()));
    //writeShdwReg(ki, state, tentry);
    tentry->operandsvalues.push_back(left);
    tentry->operandsvalues.push_back(right);
    break;
  }

  case Instruction::FPTrunc: {
    FPTruncInst *fi = cast<FPTruncInst>(i);
    Expr::Width resultType = getWidthForLLVMType(fi->getType());
    ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).concrete_value,
                                       "floating point");
    if (!fpWidthToSemantics(arg->getWidth()) || resultType > arg->getWidth())
      return terminateStateOnExecError(state, "Unsupported FPTrunc operation");

    llvm::APFloat Res(arg->getAPValue());
    bool losesInfo = false;
    Res.convert(*fpWidthToSemantics(resultType),
                llvm::APFloat::rmNearestTiesToEven,
                &losesInfo);
    //Xiaowei
    addEdge(ki, 0, state, tentry);

    bindLocal(ki, state, tentry->destvalue = ConstantExpr::alloc(Res));
    //writeShdwReg(ki, state, tentry);
    tentry->operandsvalues.push_back(arg);

    break;
  }

  case Instruction::FPExt: {
    FPExtInst *fi = cast<FPExtInst>(i);
    Expr::Width resultType = getWidthForLLVMType(fi->getType());
    ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).concrete_value,
                                        "floating point");
    if (!fpWidthToSemantics(arg->getWidth()) || arg->getWidth() > resultType)
      return terminateStateOnExecError(state, "Unsupported FPExt operation");

    llvm::APFloat Res(arg->getAPValue());
    bool losesInfo = false;
    Res.convert(*fpWidthToSemantics(resultType),
                llvm::APFloat::rmNearestTiesToEven,
                &losesInfo);
    //Xiaowei
    addEdge(ki, 0, state, tentry);

    bindLocal(ki, state, tentry->destvalue = ConstantExpr::alloc(Res));
    //writeShdwReg(ki, state, tentry);
    tentry->operandsvalues.push_back(arg);
    break;
  }

  case Instruction::FPToUI: {
    FPToUIInst *fi = cast<FPToUIInst>(i);
    Expr::Width resultType = getWidthForLLVMType(fi->getType());
    ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).concrete_value,
                                       "floating point");
    if (!fpWidthToSemantics(arg->getWidth()) || resultType > 64)
      return terminateStateOnExecError(state, "Unsupported FPToUI operation");

    llvm::APFloat Arg(arg->getAPValue());
    uint64_t value = 0;
    bool isExact = true;
    Arg.convertToInteger(&value, resultType, false,
                         llvm::APFloat::rmTowardZero, &isExact);
    //Xiaowei
    addEdge(ki, 0, state, tentry);

    bindLocal(ki, state, tentry->destvalue = ConstantExpr::alloc(value, resultType));
    //writeShdwReg(ki, state, tentry);
    tentry->operandsvalues.push_back(arg);
    break;
  }

  case Instruction::FPToSI: {
    FPToSIInst *fi = cast<FPToSIInst>(i);
    Expr::Width resultType = getWidthForLLVMType(fi->getType());
    ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).concrete_value,
                                       "floating point");
    if (!fpWidthToSemantics(arg->getWidth()) || resultType > 64)
      return terminateStateOnExecError(state, "Unsupported FPToSI operation");

    llvm::APFloat Arg(arg->getAPValue());
    uint64_t value = 0;
    bool isExact = true;
    Arg.convertToInteger(&value, resultType, false,
                         llvm::APFloat::rmTowardZero, &isExact);
    //Xiaowei
    addEdge(ki, 0, state, tentry);

    bindLocal(ki, state, tentry->destvalue = ConstantExpr::alloc(value, resultType));
    //writeShdwReg(ki, state, tentry);
    tentry->operandsvalues.push_back(arg);
    break;
  }

  case Instruction::UIToFP: {
    UIToFPInst *fi = cast<UIToFPInst>(i);
    Expr::Width resultType = getWidthForLLVMType(fi->getType());
    ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).concrete_value,
                                       "floating point");
    const llvm::fltSemantics *semantics = fpWidthToSemantics(resultType);
    if (!semantics)
      return terminateStateOnExecError(state, "Unsupported UIToFP operation");
    llvm::APFloat f(*semantics, 0);
    f.convertFromAPInt(arg->getAPValue(), false,
                       llvm::APFloat::rmNearestTiesToEven);
    //Xiaowei
    addEdge(ki, 0, state, tentry);

    bindLocal(ki, state, tentry->destvalue = ConstantExpr::alloc(f));
    //writeShdwReg(ki, state, tentry);
    tentry->operandsvalues.push_back(arg);
    break;
  }

  case Instruction::SIToFP: {
    SIToFPInst *fi = cast<SIToFPInst>(i);
    Expr::Width resultType = getWidthForLLVMType(fi->getType());
    ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).concrete_value,
                                       "floating point");
    const llvm::fltSemantics *semantics = fpWidthToSemantics(resultType);
    if (!semantics)
      return terminateStateOnExecError(state, "Unsupported SIToFP operation");
    llvm::APFloat f(*semantics, 0);
    f.convertFromAPInt(arg->getAPValue(), true,
                       llvm::APFloat::rmNearestTiesToEven);
    //Xiaowei
    addEdge(ki, 0, state, tentry);

    bindLocal(ki, state, tentry->destvalue = ConstantExpr::alloc(f));
    //writeShdwReg(ki, state, tentry);
    tentry->operandsvalues.push_back(arg);
    break;
  }

  case Instruction::FCmp: {
    FCmpInst *fi = cast<FCmpInst>(i);
    ref<ConstantExpr> left = toConstant(state, eval(ki, 0, state).concrete_value,
                                        "floating point");
    ref<ConstantExpr> right = toConstant(state, eval(ki, 1, state).concrete_value,
                                         "floating point");
    if (!fpWidthToSemantics(left->getWidth()) ||
        !fpWidthToSemantics(right->getWidth()))
      return terminateStateOnExecError(state, "Unsupported FCmp operation");

    APFloat LHS(left->getAPValue());
    APFloat RHS(right->getAPValue());
    APFloat::cmpResult CmpRes = LHS.compare(RHS);



    bool Result = false;
    switch( fi->getPredicate() ) {
      // Predicates which only care about whether or not the operands are NaNs.
    case FCmpInst::FCMP_ORD:
      Result = CmpRes != APFloat::cmpUnordered;
      break;

    case FCmpInst::FCMP_UNO:
      Result = CmpRes == APFloat::cmpUnordered;
      break;

      // Ordered comparisons return false if either operand is NaN.  Unordered
      // comparisons return true if either operand is NaN.
    case FCmpInst::FCMP_UEQ:
      if (CmpRes == APFloat::cmpUnordered) {
        Result = true;
        break;
      }
    case FCmpInst::FCMP_OEQ:
      Result = CmpRes == APFloat::cmpEqual;
      break;

    case FCmpInst::FCMP_UGT:
      if (CmpRes == APFloat::cmpUnordered) {
        Result = true;
        break;
      }
    case FCmpInst::FCMP_OGT:
      Result = CmpRes == APFloat::cmpGreaterThan;
      break;

    case FCmpInst::FCMP_UGE:
      if (CmpRes == APFloat::cmpUnordered) {
        Result = true;
        break;
      }
    case FCmpInst::FCMP_OGE:
      Result = CmpRes == APFloat::cmpGreaterThan || CmpRes == APFloat::cmpEqual;
      break;

    case FCmpInst::FCMP_ULT:
      if (CmpRes == APFloat::cmpUnordered) {
        Result = true;
        break;
      }
    case FCmpInst::FCMP_OLT:
      Result = CmpRes == APFloat::cmpLessThan;
      break;

    case FCmpInst::FCMP_ULE:
      if (CmpRes == APFloat::cmpUnordered) {
        Result = true;
        break;
      }
    case FCmpInst::FCMP_OLE:
      Result = CmpRes == APFloat::cmpLessThan || CmpRes == APFloat::cmpEqual;
      break;

    case FCmpInst::FCMP_UNE:
      Result = CmpRes == APFloat::cmpUnordered || CmpRes != APFloat::cmpEqual;
      break;
    case FCmpInst::FCMP_ONE:
      Result = CmpRes != APFloat::cmpUnordered && CmpRes != APFloat::cmpEqual;
      break;

    default:
      assert(0 && "Invalid FCMP predicate!");
    case FCmpInst::FCMP_FALSE:
      Result = false;
      break;
    case FCmpInst::FCMP_TRUE:
      Result = true;
      break;
    }

    //Xiaowei
    addEdge(ki, 0, state, tentry);
    addEdge(ki, 1, state, tentry);
    tentry->operandsvalues.push_back(left);
    tentry->operandsvalues.push_back(right);
    bindLocal(ki, state, tentry->destvalue = ConstantExpr::alloc(Result, Expr::Bool));

    //writeShdwReg(ki, state, tentry);
    // Heming: do not need to invoke bindLocalConcrete here since the results are already concrete for floating point operations,
    // and the concrete_value will be assigned correct values within bindLocal(). 
    break;
  }
 
    // Other instructions...
    // Unhandled
  case Instruction::ExtractElement:
  case Instruction::InsertElement:
  case Instruction::ShuffleVector:
    terminateStateOnError(state, "XXX vector instructions unhandled",
                          "xxx.err");
    break;
 
  default:
    terminateStateOnExecError(state, "illegal instruction");
    break;
  }

  //Xiaowei
  //slicer->printTraceEntry(tentry);
  if (SlicerExploit != 0 && slicer->getCount() == SlicerExploit){
  	  //int c = slicer->getCount();

  	  //slicer->printInsDB();
  	 // slicer->printTrace();
  	  //slicer->buildDSlice(tentry);
	  slicer->run(tentry);
	  llvm::errs() << "slicer output file is " << SlicerOutput;
	  if (SlicerOutput.compare("") == 0) {
		  llvm::errs() << "slice for the following instruction" << "\n";
		  slicer->printTraceEntry(tentry,llvm::errs());
		  slicer->printSlice(llvm::errs());
	  }
	  else {

		  std::string err;
		  raw_fd_ostream out(SlicerOutput.c_str(), err, 0);
		  if (out.has_error())
			  llvm::errs() << err;
		  else {
			  out << "slice for the following instruction" << "\n";
			  slicer->printTraceEntry(tentry,out);
			  slicer->printSlice(out);
		  }
	  }

  }
  //llvm::errs() << slicer->getPDT()->dominates(ki->inst->getParent(),ki->inst->getParent());

}

void Executor::updateStates(ExecutionState *current) {
/*  if (searcher) {
    searcher->update(current, addedStates, removedStates);
  }
  
  states.insert(addedStates.begin(), addedStates.end());
  addedStates.clear();
  
  for (std::set<ExecutionState*>::iterator
         it = removedStates.begin(), ie = removedStates.end();
       it != ie; ++it) {
    ExecutionState *es = *it;
    std::set<ExecutionState*>::iterator it2 = states.find(es);
    assert(it2!=states.end());
    states.erase(it2);
    std::map<ExecutionState*, std::vector<SeedInfo> >::iterator it3 = 
      seedMap.find(es);
    if (it3 != seedMap.end())
      seedMap.erase(it3);
    processTree->remove(es->ptreeNode);
    delete es;
  }
  removedStates.clear();*/
}

void Executor::bindInstructionConstants(KInstruction *KI) {
  GetElementPtrInst *gepi = dyn_cast<GetElementPtrInst>(KI->inst);
  if (!gepi)
    return;

  KGEPInstruction *kgepi = static_cast<KGEPInstruction*>(KI);
  ref<ConstantExpr> constantOffset =
    ConstantExpr::alloc(0, Context::get().getPointerWidth());
  uint64_t index = 1;
  for (gep_type_iterator ii = gep_type_begin(gepi), ie = gep_type_end(gepi);
       ii != ie; ++ii) {
    if (const StructType *st = dyn_cast<StructType>(*ii)) {
      const StructLayout *sl = kmodule->targetData->getStructLayout(st);
      const ConstantInt *ci = cast<ConstantInt>(ii.getOperand());
      uint64_t addend = sl->getElementOffset((unsigned) ci->getZExtValue());
      constantOffset = constantOffset->Add(ConstantExpr::alloc(addend,
                                                               Context::get().getPointerWidth()));
    } else {
      const SequentialType *set = cast<SequentialType>(*ii);
      uint64_t elementSize = 
        kmodule->targetData->getTypeStoreSize(set->getElementType());
      Value *operand = ii.getOperand();
      if (Constant *c = dyn_cast<Constant>(operand)) {
        ref<ConstantExpr> index = 
          evalConstant(c)->ZExt(Context::get().getPointerWidth());
        ref<ConstantExpr> addend = 
          index->Mul(ConstantExpr::alloc(elementSize,
                                         Context::get().getPointerWidth()));
        constantOffset = constantOffset->Add(addend);
      } else {
        kgepi->indices.push_back(std::make_pair(index, elementSize));
      }
    }
    index++;
  }
  kgepi->offset = constantOffset->getZExtValue();
}

void Executor::bindModuleConstants() {
  for (std::vector<KFunction*>::iterator it = kmodule->functions.begin(), 
         ie = kmodule->functions.end(); it != ie; ++it) {
    KFunction *kf = *it;
    for (unsigned i=0; i<kf->numInstructions; ++i)
      bindInstructionConstants(kf->instructions[i]);
  }

  kmodule->constantTable = new Cell[kmodule->constants.size()];
  for (unsigned i=0; i<kmodule->constants.size(); ++i) {
    Cell &c = kmodule->constantTable[i];
    c.value = evalConstant(kmodule->constants[i]);
    c.concrete_value = evalConstant(kmodule->constants[i]);	// Heming
  }
}

void *runForPthreadCreate(void *arg) {
  //fprintf(stderr, "Pthread %lu, tid %d is created in subroutine runForPthreadCreate\n", pthread_self(), gettid());
  executor->getMemoizer()->lock();
  assert(executor != NULL && "executor != NULL");
  ExecutionState *state = (ExecutionState *)arg;
//  fprintf(stderr, "parentState...............................\n\n\n");
//  state->addressSpace.printObjects(24);
  ExecutionState *childState = new ExecutionState(*state);
  childState->addressSpace.markLocalObjectsOnThreadStart();
  childState->pid = gettid();
  childState->coveredNew = false;
  childState->coveredLines.clear();
  childState->stateInWindow = 0;
  childState->threadLocalWindowSerialNum = 0;
  executor->getAddedStates().insert(childState);
//  fprintf(stderr, "childState...............................\n\n\n");
//  childState->addressSpace.printObjects(24);
	
  executor->getMemoizer()->unLock();
  executor->run(*childState);
  pthread_exit(0);
  return NULL;
}

bool Executor::pthreadCreate(ExecutionState *state, uint64_t *args) {
  if (executor == NULL)
    executor = (Executor *)this;
  executor_print("Pthread %lu, tid %d is is going to create pthread\n", pthread_self(), gettid());

//  fprintf(stderr, "before calls pthread_create while loop...............................\n\n\n");
//  state->addressSpace.printObjects(24);

  // wait for other threads to finish pthread_create.
  while (pthread_create_running) {
    memoizer->unLock();
    usleep(10000);
    memoizer->lock();
  }

  pthread_create_running = 1;
//  fprintf(stderr, "before calls pthread_create...............................\n\n\n");
//  state->addressSpace.printObjects(24);
  args[0] = pthread_create((pthread_t *)args[2], (const pthread_attr_t *)args[3], runForPthreadCreate, (void*)state);  

//  fprintf(stderr, "after calls pthread_create...............................\n\n\n");
//  state->addressSpace.printObjects(24);

  // wait for the child to setup semaphore.
  while (pthread_create_running) {
    memoizer->unLock();
    usleep(10000);
    memoizer->lock();
  }
  executor_print("Pthread %lu, tid %d has finished to create pthread\n", pthread_self(), gettid());
  return true;
}

void Executor::run(ExecutionState &initialState) {
  if (getpid() == gettid()) {
    bindModuleConstants();

    // Delay init till now so that ticks don't accrue during
    // optimization and such.
    initTimers();
  }
  assert(hashStates.find(gettid()) == hashStates.end());
  hashStates[gettid()] = &initialState;

  if (usingSeeds) {
    std::vector<SeedInfo> &v = seedMap[&initialState];
    
    for (std::vector<KTest*>::const_iterator it = usingSeeds->begin(), 
           ie = usingSeeds->end(); it != ie; ++it)
      v.push_back(SeedInfo(*it));

    int lastNumSeeds = usingSeeds->size()+10;
    double lastTime, startTime = lastTime = util::getWallTime();
    ExecutionState *lastState = 0;
    while (!seedMap.empty()) {
      if (haltExecution) goto dump;

      std::map<ExecutionState*, std::vector<SeedInfo> >::iterator it = 
        seedMap.upper_bound(lastState);
      if (it == seedMap.end())
        it = seedMap.begin();
      lastState = it->first;
      //unsigned numSeeds = it->second.size();
      ExecutionState &state = *lastState;
      KInstruction *ki = state.pc;
      stepInstruction(state);

      executeInstruction(state, ki);
      //processTimers(&state, MaxInstructionTime * numSeeds);
      updateStates(&state);

      if ((*stats::instructions % 1000) == 0) {
        int numSeeds = 0, numStates = 0;
        for (std::map<ExecutionState*, std::vector<SeedInfo> >::iterator
               it = seedMap.begin(), ie = seedMap.end();
             it != ie; ++it) {
          numSeeds += it->second.size();
          numStates++;
        }
        double time = util::getWallTime();
        if (SeedTime>0. && time > startTime + SeedTime) {
          klee_warning("seed time expired, %d seeds remain over %d states",
                       numSeeds, numStates);
          break;
        } else if (numSeeds<=lastNumSeeds-10 ||
                   time >= lastTime+10) {
          lastTime = time;
          lastNumSeeds = numSeeds;          
          klee_message("%d seeds remaining over: %d states", 
                       numSeeds, numStates);
        }
      }
    }

    klee_message("seeding done (%d states remain)", (int) hashStates.size());

    // XXX total hack, just because I like non uniform better but want
    // seed results to be equally weighted.
    for (Tid_To_State_Map::iterator
           it = hashStates.begin(), ie = hashStates.end();
         it != ie; ++it) {
      it->second->weight = 1.;
    }

    if (OnlySeed)
      goto dump;
  }

  //searcher = constructUserSearcher(*this);

  //searcher->update(0, states, std::set<ExecutionState*>());
/*
  while (!states.empty() && !haltExecution) {
    ExecutionState &state = searcher->selectState();
    KInstruction *ki = state.pc;
    stepInstruction(state);

    executeInstruction(state, ki);
    processTimers(&state, MaxInstructionTime);

    if (MaxMemory) {
      if ((stats::instructions & 0xFFFF) == 0) {
        // We need to avoid calling GetMallocUsage() often because it
        // is O(elts on freelist). This is really bad since we start
        // to pummel the freelist once we hit the memory cap.
        unsigned mbs = sys::Process::GetTotalMemoryUsage() >> 20;
        
        if (mbs > MaxMemory) {
          if (mbs > MaxMemory + 100) {
            // just guess at how many to kill
            unsigned numStates = states.size();
            unsigned toKill = std::max(1U, numStates - numStates*MaxMemory/mbs);

            if (MaxMemoryInhibit)
              klee_warning("killing %d states (over memory cap)",
                           toKill);

            std::vector<ExecutionState*> arr(states.begin(), states.end());
            for (unsigned i=0,N=arr.size(); N && i<toKill; ++i,--N) {
              unsigned idx = rand() % N;

              // Make two pulls to try and not hit a state that
              // covered new code.
              if (arr[idx]->coveredNew)
                idx = rand() % N;

              std::swap(arr[idx], arr[N-1]);
              terminateStateEarly(*arr[N-1], "memory limit");
            }
          }
          atMemoryLimit = true;
        } else {
          atMemoryLimit = false;
        }
      }
    }

    updateStates(&state);
  }
*/

  memoizer->lock();
  while (!haltExecution) {
    ExecutionState &state = *(hashStates[gettid()]);
	if (state.pid == -1) {
	  fprintf(stderr, "Thread %d exits from run() with stack depth %u\n", gettid(), state.pthreadCreateStackDepth);
       fflush(stderr);
	  memoizer->unLock();
	  return;
	}
    KInstruction *ki = state.pc;
/*    if (ki->inst->getParent()->getParent()->getNameStr() != "memset") {
      errs() << "Tid " << gettid() <<  " run Inst " << *(ki->inst) 
  			<< " in func " << ki->inst->getParent()->getParent()->getNameStr() 
  			<< " in BB " << ki->inst->getParent()->getNameStr() << "\n";
    }*/
    if (state.threadStopInst == state.pc) {
      state.pthreadCreateStackDepth -= state.stack.size();
      executor_print("Tid %d check terminate %u\n", gettid(), state.pthreadCreateStackDepth);
      if (state.pthreadCreateStackDepth == 0) {
//        cerr << "Inst " << *ki->inst << "\n";
         /*fprintf(stderr, "Tid %d should terminate thread execution function %s, BB %s\n", gettid(), 
           ki->inst->getParent()->getParent()->getNameStr().c_str(), 
           ki->inst->getParent()->getNameStr().c_str());*/
         fflush(stderr);
	     state.addressSpace.markLocalObjectsOnThreadExit();
         terminateStateEarly(state, "terminate thread execution");
         memoizer->unLock();
         return;
	  }
    }
    stepInstruction(state);
    executeInstruction(state, ki);
    memoizer->unLock();
    //sched_yield();
    //usleep(1);
    memoizer->lock();
  }
  memoizer->unLock();

  delete searcher;
  searcher = 0;
  
 dump:
  if (DumpStatesOnHalt && !states_empty()) {
    std::cerr << "KLEE: halting execution, dumping remaining states\n";
    for (Tid_To_State_Map::iterator
           it = hashStates.begin(), ie = hashStates.end();
         it != ie; ++it) {
      ExecutionState &state = *(it->second);
      stepInstruction(state); // keep stats rolling
      terminateStateEarly(state, "execution halting");
    }
    updateStates(0);
  }
}

std::string Executor::getAddressInfo(ExecutionState &state, 
                                     ref<Expr> address) const{
  std::ostringstream info;
  info << "\taddress: " << address << "\n";
  uint64_t example;
  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(address)) {
    example = CE->getZExtValue();
  } else {
    ref<ConstantExpr> value;
    bool success = solver->getValue(state, address, value);
    assert(success && "FIXME: Unhandled solver failure");
    (void) success;
    example = value->getZExtValue();
    info << "\texample: " << example << "\n";
    std::pair< ref<Expr>, ref<Expr> > res = solver->getRange(state, address);
    info << "\trange: [" << res.first << ", " << res.second <<"]\n";
  }
  
  MemoryObject hack((unsigned) example);    
  MemoryMap::iterator lower = state.addressSpace.objects.upper_bound(&hack);
  info << "\tnext: ";
  if (lower==state.addressSpace.objects.end()) {
    info << "none\n";
  } else {
    const MemoryObject *mo = lower->first;
    std::string alloc_info;
    mo->getAllocInfo(alloc_info);
    info << "object at " << mo->address
         << " of size " << mo->size << "\n"
         << "\t\t" << alloc_info << "\n";
  }
  if (lower!=state.addressSpace.objects.begin()) {
    --lower;
    info << "\tprev: ";
    if (lower==state.addressSpace.objects.end()) {
      info << "none\n";
    } else {
      const MemoryObject *mo = lower->first;
      std::string alloc_info;
      mo->getAllocInfo(alloc_info);
      info << "object at " << mo->address 
           << " of size " << mo->size << "\n"
           << "\t\t" << alloc_info << "\n";
    }
  }

  return info.str();
}

void Executor::terminateState(ExecutionState &state) {
  //fprintf(stderr, "Executor::terminateState tid %d self %x\n", gettid(), (int)pthread_self());
  if (replayOut && replayPosition!=replayOut->numObjects) {
    klee_warning_once(replayOut, 
                      "replay did not consume all objects in test input.");
  }

  interpreterHandler->incPathsExplored();

  std::set<ExecutionState*>::iterator it = addedStates.find(&state);
  if (it==addedStates.end()) {
    state.pc = state.prevPC;

    removedStates.insert(&state);
  } else {
    // never reached searcher, just delete immediately
    std::map< ExecutionState*, std::vector<SeedInfo> >::iterator it3 = 
      seedMap.find(&state);
    if (it3 != seedMap.end())
      seedMap.erase(it3);
    addedStates.erase(it);
    //Heming comment this.
    //processTree->remove(state.ptreeNode);
    //delete &state;
  }
}

void Executor::terminateStateEarly(ExecutionState &state, 
                                   const Twine &message) {
  /*if (!OnlyOutputStatesCoveringNew || state.coveredNew ||
      (AlwaysOutputSeeds && seedMap.count(&state)))
    interpreterHandler->processTestCase(state, (message + "\n").str().c_str(),
                                        "early");*/
#ifdef MEMOIZER_ORDER
  memoizer->threadExit(&(state.pid), 0);
#endif
  terminateState(state);
}

void Executor::terminateStateOnExit(ExecutionState &state, int exitValue) {
  fprintf(stderr, "enter Executor::terminateStateOnExit with value %d\n", exitValue);
  fflush(stderr);

  /*if (!OnlyOutputStatesCoveringNew || state.coveredNew || 
      (AlwaysOutputSeeds && seedMap.count(&state)))
    interpreterHandler->processTestCase(state, 0, 0);*/

#ifdef MEMOIZER_ORDER
  if (IS_BATCH_PROGRAM) {
    memoizer->taskEnd(&(state.threadLocalWindowSerialNum), 0, 0);
  }
  memoizer->appEnd(&(state.pid));
#endif
  terminateState(state);

  // Heming: since we do not need any KLEE associated solving constraints at the end of a program,
  // we can and should (for the httpd parent process) call exit directly here.
  //fprintf(stderr, "Executor::terminateStateOnExit with value %d, getCnt %ld\n", exitValue, getCnt());
  fflush(stderr);
  exit(exitValue);
}

void Executor::terminateStateOnError(ExecutionState &state,
                                     const llvm::Twine &messaget,
                                     const char *suffix,
                                     const llvm::Twine &info) {
  std::string message = messaget.str();
  static std::set< std::pair<Instruction*, std::string> > emittedErrors;
  const InstructionInfo &ii = *state.prevPC->info;
  
  if (EmitAllErrors ||
      emittedErrors.insert(std::make_pair(state.prevPC->inst, message)).second) {
    if (ii.file != "") {
      klee_message("ERROR: %s:%d: %s", ii.file.c_str(), ii.line, message.c_str());
    } else {
      klee_message("ERROR: %s", message.c_str());
    }
    if (!EmitAllErrors)
      klee_message("NOTE: now ignoring this error at this location");
    
    std::ostringstream msg;
    msg << "Error: " << message << "\n";
    if (ii.file != "") {
      msg << "File: " << ii.file << "\n";
      msg << "Line: " << ii.line << "\n";
    }
    msg << "Stack: \n";
    state.dumpStack(msg);

    std::string info_str = info.str();
    if (info_str != "")
      msg << "Info: \n" << info_str;
    //interpreterHandler->processTestCase(state, msg.str().c_str(), suffix);
  }
    
  terminateState(state);
}

// XXX shoot me
static const char *okExternalsList[] = { "printf", 
                                         "fprintf", 
                                         "puts",
                                         "getpid" };
static std::set<std::string> okExternals(okExternalsList,
                                         okExternalsList + 
                                         (sizeof(okExternalsList)/sizeof(okExternalsList[0])));

void Executor::executeTernBeforeLandmark(ExecutionState &state, int hookId, std::vector<ref<Expr> > &hookArgs) {
  uint64_t *args = (uint64_t*) alloca(sizeof(*args) * (LANDMARK_HOOK_ARG_SIZE + 1));
  memset(args, 0, sizeof(*args) * (LANDMARK_HOOK_ARG_SIZE + 1));
  unsigned i = 2;
  uint64_t landmarkIndex = 10000;

  //fprintf(stderr, "hookArgs size %u\n", hookArgs.size());
  for (std::vector<ref<Expr> >::iterator ai = hookArgs.begin(), 
         ae = hookArgs.end(); ai!=ae; ++ai) {
    if (AllowExternalSymCalls) { // don't bother checking uniqueness
      ref<ConstantExpr> ce;
      bool success = solver->getValue(state, *ai, ce);
      assert(success && "FIXME: Unhandled solver failure");
      if (ai == hookArgs.begin()) {
        static_cast<ConstantExpr*>(ce.get())->toMemory((void*) &landmarkIndex);	
        //fprintf(stderr, "landmarkIndex value %llu\n", landmarkIndex);
        continue;
      }
				
      static_cast<ConstantExpr*>(ce.get())->toMemory((void*) &args[i]);
      i++;
      (void) success;
    } else {
      ref<Expr> arg = toUnique(state, *ai);
      if (ConstantExpr *CE = dyn_cast<ConstantExpr>(arg)) {
        // XXX kick toMemory functions from here
        if (ai == hookArgs.begin()) {
          CE->toMemory((void*) &landmarkIndex);
          //fprintf(stderr, "landmarkIndex value %llu, landmark %s\n", landmarkIndex, landmarks[landmarkIndex]);
          continue;
        }
					
        CE->toMemory((void*) &args[i]);
        i++;
      } else {
        terminateStateOnExecError(state, 
                                  "executeTernBeforeLandmark with symbolic argument.");
        return;
      }
    }
  }

  //fprintf(stderr, "enter executeTernBeforeLandmark %llx, %llx, %llx, %llx\n", args[0], args[1], args[2], args[3]);
  assert(landmarkIndex != 10000);
  KInstruction *ki = state.prevPC;
  int inst_id = exeInstIDs[(long)(ki->inst)];
  memoizer->beforeLandmark(landmarkIndex, hookId, inst_id, (uint64_t)args, (uint64_t)ki, 0/*, memoizer->getCallStackStr(state)*/);
}

void Executor::executeTernAfterLandmark(ExecutionState &state, int hookId, std::vector<ref<Expr> > &hookArgs) {
  uint64_t *args = (uint64_t*) alloca(sizeof(*args) * (LANDMARK_HOOK_ARG_SIZE + 1));
  memset(args, 0, sizeof(*args) * (LANDMARK_HOOK_ARG_SIZE + 1));
  unsigned i = 0;														// include the return value, this is different from the i in executeTernBeforeLandmark.
  uint64_t landmarkIndex = 10000;

  for (std::vector<ref<Expr> >::iterator ai = hookArgs.begin(), 
         ae = hookArgs.end(); ai!=ae; ++ai) {
    if (AllowExternalSymCalls) { // don't bother checking uniqueness
      ref<ConstantExpr> ce;
      bool success = solver->getValue(state, *ai, ce);
      assert(success && "FIXME: Unhandled solver failure");
      if (ai == hookArgs.begin()) {
        static_cast<ConstantExpr*>(ce.get())->toMemory((void*) &landmarkIndex);		
        continue;
      }
				
      static_cast<ConstantExpr*>(ce.get())->toMemory((void*) &args[i]);
      if (i == 0)
        i += 2;
      else
        i++;
      (void) success;
    } else {
      ref<Expr> arg = toUnique(state, *ai);
      if (ConstantExpr *CE = dyn_cast<ConstantExpr>(arg)) {
        // XXX kick toMemory functions from here
        if (ai == hookArgs.begin()) {
          CE->toMemory((void*) &landmarkIndex);
          //fprintf(stderr, "landmarkIndex value %llu\n", landmarkIndex);
          continue;
        }

        CE->toMemory((void*) &args[i]);
        if (i == 0)
          i += 2;
        else
          i++;
      } else {
        terminateStateOnExecError(state, 
                                  "executeTernAfterLandmark with symbolic argument.");
        return;
      }
    }
  }

  //fprintf(stderr, "tid %d enter executeTernAfterLandmark %llx, callStack:\n", gettid(), landmarkIndex);
  //printKLEECallStack(state);
	
  assert(landmarkIndex != 10000);
  KInstruction *ki = state.prevPC;
  long inst_id = exeInstIDs[(long)(ki->inst)];
  memoizer->afterLandmark(0, landmarkIndex, hookId, inst_id, 0, (uint64_t)args, (uint64_t)ki, 0/*, memoizer->getCallStackStr(state)*/);
}

void Executor::callExternalFunction(ExecutionState &state,
                                    KInstruction *target,
                                    Function *function,
                                    std::vector< ref<Expr> > &arguments
                                    ) {
  assert(function && function->hasName());
  std::string funcName = function->getNameStr();

  // check if specialFunctionHandler wants it
  if (specialFunctionHandler->handle(state, function, target, arguments))
    return;

  // YJF: handle dl* functions on bc libs
  if(bclib->callDLFunction(state, target, function, arguments))
    return;
  
  if (NoExternals && !okExternals.count(function->getName())) {
    std::cerr << "KLEE:ERROR: Calling not-OK external function : " 
               << function->getNameStr() << "\n";
    terminateStateOnError(state, "externals disallowed", "user.err");
    return;
  }

  // normal external function handling path
  // allocate 128 bits for each argument (+return value) to support fp80's;
  // we could iterate through all the arguments first and determine the exact
  // size we need, but this is faster, and the memory usage isn't significant.
  uint64_t *args = (uint64_t*) alloca(2*sizeof(*args) * (arguments.size() + 1));
  memset(args, 0, 2 * sizeof(*args) * (arguments.size() + 1));
  unsigned wordIndex = 2;
  for (std::vector<ref<Expr> >::iterator ai = arguments.begin(), 
       ae = arguments.end(); ai!=ae; ++ai) {
    if (AllowExternalSymCalls) { // don't bother checking uniqueness
      ref<ConstantExpr> ce;
      bool success = solver->getValue(state, *ai, ce);
      assert(success && "FIXME: Unhandled solver failure");
      (void) success;
      ce->toMemory(&args[wordIndex]);
      wordIndex += (ce->getWidth()+63)/64;
    } else {
      ref<Expr> arg = toUnique(state, *ai);
      if (ConstantExpr *ce = dyn_cast<ConstantExpr>(arg)) {
        // XXX kick toMemory functions from here
        ce->toMemory(&args[wordIndex]);
        wordIndex += (ce->getWidth()+63)/64;
      } else {
        terminateStateOnExecError(state, 
                                  "external call with symbolic argument: " + 
                                  function->getName());
        return;
      }
    }
  }

  int oldStackSize = 0;
  if (funcName == "pthread_create") {
    Instruction *Inst = target->inst;
    if (Inst->getOpcode()==Instruction::Call) {
      CallSite CS  = CallSite(cast<CallInst>(Inst));
      KInstIterator kitr = state.pc;
      ++kitr;
      ++kitr;
      state.subRoutine = kitr;
      //state.pthreadCreateStackDepth += state.stack.size();
      oldStackSize = state.pthreadCreateStackDepth;
      state.pthreadCreateStackDepth = state.stack.size();
      executor_print("before pthread_create: state.subRoutine %p,stack depth %u\n", (void *)state.subRoutine, state.pthreadCreateStackDepth);
    }
  }

  bool success = true;
  if (funcName == "pthread_create") {
    success = pthreadCreate(&state, args);
  } else {
    if (funcName == "pthread_exit") {
#ifdef MEMOIZER_ORDER
      memoizer->threadExit(&(state.pid), 0, true);
#endif
    }
    success = externalDispatcher->executeCall(function, target->inst, args, memoizer->getMutex());
  }

  if (!success) {
		if (function->getNameStr() != "pthread_kill") {
    			terminateStateOnError(state, "failed external call: " + function->getName(),
                          "external.err");
					executor_print("pid %d returns from callExternalFunction-1\n", gettid());
    			return;
		} else
		  fprintf(stderr, "WARN: pthread_kill fails\n");
					
  }
  if (funcName == "pthread_create") {
    // Heming: this is necessary for my new pthread_create approach.
    ++state.pc;
    ++state.pc;
    ++state.pc;
    state.pthreadCreateStackDepth = oldStackSize;
  }

/*
  state.addressSpace.copyOutConcretes();
  if (!SuppressExternalWarnings) {
    std::ostringstream os;
    os << "calling external: " << function->getNameStr() << "(";
    for (unsigned i=0; i<arguments.size(); i++) {
      os << arguments[i];
      if (i != arguments.size()-1)
	os << ", ";
    }
    os << ")";
    
    if (AllExternalWarnings)
      klee_warning("%s", os.str().c_str());
    else
      klee_warning_once(function, "%s", os.str().c_str());
  }


  
  bool success = externalDispatcher->executeCall(function, target->inst, args);
  if (!success) {
    terminateStateOnError(state, "failed external call: " + function->getName(),
                          "external.err");
    return;
  }

  if (!state.addressSpace.copyInConcretes()) {
    terminateStateOnError(state, "external modified read-only object",
                          "external.err");
    return;
  }
*/
  const Type *resultType = target->inst->getType();
  if (resultType != Type::getVoidTy(getGlobalContext())) {
    ref<Expr> e = ConstantExpr::fromMemory((void*) args, 
                                           getWidthForLLVMType(resultType));
    bindLocal(target, state, e);
  }
  ternHandleSpecialFunctions(state, funcName.c_str(), args);
}

/***/

ref<Expr> Executor::replaceReadWithSymbolic(ExecutionState &state, 
                                            ref<Expr> e) {
  unsigned n = interpreterOpts.MakeConcreteSymbolic;
  if (!n || replayOut || replayPath)
    return e;

  // right now, we don't replace symbolics (is there any reason too?)
  if (!isa<ConstantExpr>(e))
    return e;

  if (n != 1 && random() %  n)
    return e;

  // create a new fresh location, assert it is equal to concrete value in e
  // and return it.
  
  static unsigned id;
  const Array *array = new Array("rrws_arr" + llvm::utostr(++id), 
                                 Expr::getMinBytesForWidth(e->getWidth()));
  ref<Expr> res = Expr::createTempRead(array, e->getWidth());
  ref<Expr> eq = NotOptimizedExpr::create(EqExpr::create(e, res));
  std::cerr << "Making symbolic: " << eq << "\n";
  state.addConstraint(eq);
  return res;
}

ObjectState *Executor::bindObjectInState(ExecutionState &state, 
                                         const MemoryObject *mo,
                                         bool isLocal,
                                         const Array *array) {
  long int_mo2 = (long)mo;
  MemoryObject *mo2 = (MemoryObject *)int_mo2;
  ObjectState *os = array ? new ObjectState(mo2, array) : new ObjectState(mo2);
  if (array)
    assert(os->isKnownSymbolic());
  // Heming copy concrete value before it is marked as symbolic.
  // Heming: this is a very important hack to klee, without this, symbolic var does not have init concrete value.
  if (array) {
    const ObjectState *oldOs = state.addressSpace.findObject(mo);
    assert(oldOs != NULL && "mo can not be NULL");
    memcpy(os->concreteStore, oldOs->concreteStore, mo->size);
    //fprintf(stderr, "bindObjectInState copy concrete %s for symbolic var %s\n", (char *)os->concreteStore, array->name.c_str());
  }
  state.addressSpace.bindObject(mo, os);

  // Its possible that multiple bindings of the same mo in the state
  // will put multiple copies on this list, but it doesn't really
  // matter because all we use this list for is to unbind the object
  // on function return.
  if (isLocal)
    state.stack.back().allocas.push_back(mo);

  return os;
}

/* Heming: when doing mix concrete/symbolic executioin for executeAlloc, just need to handle 
     the concrete operation of executeAlloc and ignore the symbolic one.
     This means that the size passed to this function must be a concrete value, and the executeInstruction
     function must only pass the concrete version of the value to this function.
*/
void Executor::executeAlloc(ExecutionState &state,
                            ref<Expr> size,
                            bool isLocal,
                            KInstruction *target,
                            bool zeroMemory,
                            const ObjectState *reallocFrom
                            ) {
  // Heming added assertion.
  assert(isa<ConstantExpr>(size) && "executeAlloc: TERN is doing mix concrete/symbolic operation, so only needs to handle constant expr");

  size = toUnique(state, size);
  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(size)) {
    MemoryObject *mo = memory->allocate(CE->getZExtValue(), isLocal, false, 
                                        state.prevPC->inst);
    if (!mo) {
      bindLocal(target, state, 
                ConstantExpr::alloc(0, Context::get().getPointerWidth()));

      //Xiaowei
      //writeShdwReg(target, state, target->te);

    } else {
      ObjectState *os = bindObjectInState(state, mo, isLocal);
      if (zeroMemory) {
        os->initializeToZero();
      } else {
        os->initializeToRandom();
      }
      bindLocal(target, state, mo->getBaseExpr());
      
      //Xiaowei
      //writeShdwReg(target, state, target->te);

      if (reallocFrom) {
        unsigned count = std::min(reallocFrom->size, os->size);
        for (unsigned i=0; i<count; i++)
          os->write(i, reallocFrom->read8(i));
        state.addressSpace.unbindObject(reallocFrom->getObject());
      }
    }
  } else {
    // XXX For now we just pick a size. Ideally we would support
    // symbolic sizes fully but even if we don't it would be better to
    // "smartly" pick a value, for example we could fork and pick the
    // min and max values and perhaps some intermediate (reasonable
    // value).
    // 
    // It would also be nice to recognize the case when size has
    // exactly two values and just fork (but we need to get rid of
    // return argument first). This shows up in pcre when llvm
    // collapses the size expression with a select.
    assert(false && "TERN does not handle this2");
    ref<ConstantExpr> example;
    bool success = solver->getValue(state, size, example);
    assert(success && "FIXME: Unhandled solver failure");
    (void) success;
    
    // Try and start with a small example.
    Expr::Width W = example->getWidth();
    while (example->Ugt(ConstantExpr::alloc(128, W))->isTrue()) {
      ref<ConstantExpr> tmp = example->LShr(ConstantExpr::alloc(1, W));
      bool res;
      bool success = solver->mayBeTrue(state, EqExpr::create(tmp, size), res);
      assert(success && "FIXME: Unhandled solver failure");      
      (void) success;
      if (!res)
        break;
      example = tmp;
    }

    StatePair fixedSize = fork(state, EqExpr::create(example, size), true);
    
    if (fixedSize.second) { 
      // Check for exactly two values
      ref<ConstantExpr> tmp;
      bool success = solver->getValue(*fixedSize.second, size, tmp);
      assert(success && "FIXME: Unhandled solver failure");      
      (void) success;
      bool res;
      success = solver->mustBeTrue(*fixedSize.second, 
                                   EqExpr::create(tmp, size),
                                   res);
      assert(success && "FIXME: Unhandled solver failure");      
      (void) success;
      if (res) {
        executeAlloc(*fixedSize.second, tmp, isLocal,
                     target, zeroMemory, reallocFrom);
      } else {
        // See if a *really* big value is possible. If so assume
        // malloc will fail for it, so lets fork and return 0.
        StatePair hugeSize = 
          fork(*fixedSize.second, 
               UltExpr::create(ConstantExpr::alloc(1<<31, W), size), 
               true);
        if (hugeSize.first) {
          klee_message("NOTE: found huge malloc, returing 0");
          bindLocal(target, *hugeSize.first, 
                    ConstantExpr::alloc(0, Context::get().getPointerWidth()));
        }
        
        if (hugeSize.second) {
          std::ostringstream info;
          ExprPPrinter::printOne(info, "  size expr", size);
          info << "  concretization : " << example << "\n";
          info << "  unbound example: " << tmp << "\n";
          terminateStateOnError(*hugeSize.second, 
                                "concretized symbolic size", 
                                "model.err", 
                                info.str());
        }
      }
    }

    if (fixedSize.first) // can be zero when fork fails
      executeAlloc(*fixedSize.first, example, isLocal, 
                   target, zeroMemory, reallocFrom);
  }
}

/* Heming: when doing mix concrete/symbolic executioin for executeFree, just need to handle 
     the concrete operation of executeFree and ignore the symbolic one.
     This means that the address passed to this function must be a concrete value, and the executeInstruction
     function must only pass the concrete version of the value to this function.
*/
void Executor::executeFree(ExecutionState &state,
                           ref<Expr> address,
                           KInstruction *target) {
  // Heming
  assert(isa<ConstantExpr>(address) && "executeFree: TERN is doing mix concrete/symbolic operation, so only needs to handle constant expr");
  //fprintf(stderr, "executeFree addr %llx\n", cast<ConstantExpr>(address)->getZExtValue());
  //StatePair zeroPointer = fork(state, Expr::createIsZero(address), true);
  if (cast<ConstantExpr>(address)->getZExtValue() == 0) {
    //fprintf(stderr, "WARN Executor::executeFree: freeing zero 0\n");
    return;
  }
  StatePair zeroPointer;
  zeroPointer.first = NULL;
  zeroPointer.second = &state;

  if (zeroPointer.first) {
    if (target)
      bindLocal(target, *zeroPointer.first, Expr::createPointer(0));
  }
  if (zeroPointer.second) { // address != 0
    ExactResolutionList rl;
    resolveExact(*zeroPointer.second, address, rl, "free");
    
    for (Executor::ExactResolutionList::iterator it = rl.begin(), 
           ie = rl.end(); it != ie; ++it) {
      const MemoryObject *mo = it->first.first;
      if (mo->isLocal) {
        terminateStateOnError(*it->second, 
                              "free of alloca", 
                              "free.err",
                              getAddressInfo(*it->second, address));
      } else if (mo->isGlobal) {
        terminateStateOnError(*it->second, 
                              "free of global", 
                              "free.err",
                              getAddressInfo(*it->second, address));
      } else {
        it->second->addressSpace.unbindObject(mo);
        if (target)
          bindLocal(target, *it->second, Expr::createPointer(0));
      }
    }
  }
}

void Executor::resolveExact(ExecutionState &state,
                            ref<Expr> p,
                            ExactResolutionList &results, 
                            const std::string &name) {
  // XXX we may want to be capping this?
  ResolutionList rl;
  state.addressSpace.resolve(state, solver, p, rl);
  
  assert(rl.size() <= 1 && "TERN: resolveExact, since p is constant, the size of rl must equal 1");
  if (rl.size() == 1)
    results.push_back(std::make_pair(*(rl.begin()), &state));
/*
  ExecutionState *unbound = &state;
  for (ResolutionList::iterator it = rl.begin(), ie = rl.end(); 
       it != ie; ++it) {
    ref<Expr> inBounds = EqExpr::create(p, it->first->getBaseExpr());
    
    StatePair branches = fork(*unbound, inBounds, true);
    
    if (branches.first)
      results.push_back(std::make_pair(*it, branches.first));

    unbound = branches.second;
    if (!unbound) // Fork failure
      break;
  }

  if (unbound) {
    terminateStateOnError(*unbound,
                          "memory error: invalid pointer: " + name,
                          "ptr.err",
                          getAddressInfo(*unbound, p));
  }*/
}

void Executor::executeMemoryOperation(ExecutionState &state,
                                      bool isWrite,
                                      ref<Expr> address,
                                      ref<Expr> value /* undef if read */,
                                      KInstruction *target /* undef if write */, bool isConcreteOp) {
  Expr::Width type = (isWrite ? value->getWidth() : 
                     getWidthForLLVMType(target->inst->getType()));
  unsigned bytes = Expr::getMinBytesForWidth(type);
  ref<Expr> new_value, old_value;

  //Xiaowei
  ConstantExpr *CE = dyn_cast<ConstantExpr>(address);
  uint64_t addr = CE->getZExtValue();
  if (isWrite) {
	  for (unsigned i=0;i<bytes;i++)
	  {
		  slicer->writeShdwmem(addr+i,slicer->get_cur_te());
	  }
  } else {

	  for (unsigned i=0;i<bytes;i++)
	  {
		  slicer->get_cur_te()->defuse.insert(slicer->readShdwmem(addr+i));
	  }
  }

  if (SimplifySymIndices) {
    if (!isa<ConstantExpr>(address))
      address = state.constraints.simplifyExpr(address);
    if (isWrite && !isa<ConstantExpr>(value))
      value = state.constraints.simplifyExpr(value);
  }

  // fast path: single in-bounds resolution
  ObjectPair op;
  bool success = true;
  bool inBounds;

  solver->setTimeout(stpTimeout);
  if (!state.addressSpace.resolveOne(state, solver, address, op, success)) {
    assert(false);						// Heming blocks this branch.
    address = toConstant(state, address, "resolveOne failure");
    success = state.addressSpace.resolveOne(cast<ConstantExpr>(address), op);
  }
  solver->setTimeout(0);

  // Heming added this: if use tree search, fail, then we just use linear search to the address space.
  if (!success) {
    if (isa<ConstantExpr>(address)) {
      uint64_t addr = cast<ConstantExpr>(address)->getZExtValue();
      if (state.addressSpace.myFindObject(addr, op)) {
        fprintf(stderr, "Tid %d failed but findObject got it %llx\n", gettid(), addr);
	    success = true;
      } else
        fprintf(stderr, "Tid %d failed and findObject can not got it %llx\n", gettid(), addr);
    }
  }

  // Heming: add this to tolerate the memcpy in my_realloc in mysql-6.0.5-alpha. The new allocated size of pointer is longer than
  // existing size in oldpointer, so memcpy failed in KLEE.
  if (!success && !isWrite) {
    bindLocal(target, state, ConstantExpr::alloc(RANDOM_BAD_CONSTANT, type));
    return;
  }

  if (success) {
    const MemoryObject *mo = op.first;

    if (MaxSymArraySize && mo->size>=MaxSymArraySize) {
      assert(false);			// Heming blocks this branch.
      address = toConstant(state, address, "max-sym-array-size");
    }
    
    ref<Expr> offset = mo->getOffsetExpr(address);

    solver->setTimeout(stpTimeout);
    bool success = solver->mustBeTrue(state, 
                                      mo->getBoundsCheckOffset(offset, bytes),
                                      inBounds);
    solver->setTimeout(0);
    if (!success) {
      state.pc = state.prevPC;
      terminateStateEarly(state, "query timed out");
      return;
    }

    if (inBounds) {
      if (RECORD_MEM_ACCESS) {
        assert(isa<ConstantExpr>(address));
        memoizer->recordMemAccess(mo->isLocal, state, target, (int)cast<ConstantExpr>(address)->getZExtValue(32), exeInstIDs[(long)(target->inst)]);
      }

      const ObjectState *os = op.second;
      if (isWrite) {
        if (os->readOnly) {
//          fprintf(stderr, "WARN: executeMemoryOperation1 readonly %llx, %u\n", mo->address, mo->size);
        }

        // YJF: get value overwritten by a write
        old_value = os->readConcrete(offset, type);
        new_value = value;

        long int_os2 = (long)os;
        ObjectState *os2 = (ObjectState *)int_os2;
        ObjectState *wos = state.addressSpace.getWriteable(mo, os2);
        if (!isConcreteOp)
          wos->write(offset, value);
        else
          wos->writeConcrete(offset, value);       

      } else {
        ref<Expr> result = os->read(offset, type);
        // Heming add this check to avoid un-init value.
        if (isa<ConstantExpr>(result)) {
		 if (0xabababab == cast<ConstantExpr>(address)->getZExtValue()) {
            fprintf(stderr, "LOAD UN-INIT-ED VALUE, MAYBE A BUG FROM APPLICATION\n");
            assert(false);
          }
        }
        
        if (interpreterOpts.MakeConcreteSymbolic)
          result = replaceReadWithSymbolic(state, result);
        
        bindLocal(target, state, result);

        // Heming
        if (!isa<ConstantExpr>(result)) {
          executor_print("WARN: TERN concretize result for load\n");          
          result = os->readConcrete(offset, type);
          bindLocalConcrete(target, state, result);  
        }

        // YJF: get read result
        new_value = result;
      }

      // YJF: hook for race detector.  For now, only look at
      // value->getWidth(); may use contents of value in the future, in
      // case two threads write the same value.
      //
      // YJF: why two flags isGlobal and isLocal?
      // 
      if(get_option(tern, detect_race) && (mo->isGlobal||!mo->isLocal)) {
          if(!get_option(tern, one_race_only) 
             || !theRaceDetector->raceDetected()) {
              pid_t tid = gettid();
              theRaceDetector->onMemoryAccess(state, memoizer->ternMyTid(tid), 
                                              isWrite, mo, offset, bytes,
                                              new_value, old_value);
          }
      }
      return;
    }
  } 

  fprintf(stderr, "\nTid %d Failed to resolve addr %llx, isWrite %d, success %d, inBounds %d\n", gettid(), cast<ConstantExpr>(address)->getZExtValue(), isWrite, success, inBounds);
  if (target) {
    errs() << "executeMemoryOperation Inst " << *(target->inst) << "\n";
    fprintf(stderr, "Called function is %s, BB is %s\n", 
			target->inst->getParent()->getParent()->getNameStr().c_str(),
			target->inst->getParent()->getNameStr().c_str());
  }
  printKLEECallStack(state);
  fflush(stderr);
  return;
  //assert(false);

  // we are on an error path (no resolution, multiple resolution, one
  // resolution with out of bounds)
  
  ResolutionList rl;  
  solver->setTimeout(stpTimeout);
  bool incomplete = state.addressSpace.resolve(state, solver, address, rl,
                                               0, stpTimeout);
  solver->setTimeout(0);
  
  // XXX there is some query wasteage here. who cares?
  ExecutionState *unbound = &state;
  
  for (ResolutionList::iterator i = rl.begin(), ie = rl.end(); i != ie; ++i) {
    const MemoryObject *mo = i->first;
    const ObjectState *os = i->second;
    ref<Expr> inBounds = mo->getBoundsCheckPointer(address, bytes);
    
    StatePair branches = fork(*unbound, inBounds, true);
    ExecutionState *bound = branches.first;

    // bound can be 0 on failure or overlapped 
    if (bound) {
      if (isWrite) {
        if (os->readOnly) {
          //fprintf(stderr, "WARN: executeMemoryOperation2 readonly %llx, %u\n", mo->address, mo->size);
        }
        long int_os2 = (long)os;
        ObjectState *os2 = (ObjectState *)int_os2;
        ObjectState *wos = bound->addressSpace.getWriteable(mo, os2);
        wos->write(mo->getOffsetExpr(address), value);
      } else {
        ref<Expr> result = os->read(mo->getOffsetExpr(address), type);
        bindLocal(target, *bound, result);
      }
    }

    unbound = branches.second;
    if (!unbound)
      break;
  }
  
  // XXX should we distinguish out of bounds and overlapped cases?
  if (unbound) {
    if (incomplete) {
      terminateStateEarly(*unbound, "query timed out (resolve)");
    } else {
      terminateStateOnError(*unbound,
                            "memory error: out of bound pointer",
                            "ptr.err",
                            getAddressInfo(*unbound, address));
    }
  }
}

void Executor::executeMakeSymbolic(ExecutionState &state, 
                                   const MemoryObject *mo) {

#ifdef MEMOIZER_ORDER
  // Heming: if not in task region, then view it as NOP.
  if (!memoizer->threadInTask()) {
    return;
  }
#endif
																	
  // Create a new object state for the memory object (instead of a copy).
  if (!replayOut) {
    const Array *array = new Array(mo->name + llvm::utostr(memoizer->mmzEnterTaskOrder()), mo->size);
    bindObjectInState(state, mo, false, array);
    state.addSymbolic(mo, array);
    schedCache->addSymVar(array);
    memoizer->mmzTaskConcreteBytes((void *)mo->address);
    
    std::map< ExecutionState*, std::vector<SeedInfo> >::iterator it = 
      seedMap.find(&state);
    if (it!=seedMap.end()) { // In seed mode we need to add this as a
                             // binding.
      for (std::vector<SeedInfo>::iterator siit = it->second.begin(), 
             siie = it->second.end(); siit != siie; ++siit) {
        SeedInfo &si = *siit;
        KTestObject *obj = si.getNextInput(mo, NamedSeedMatching);

        if (!obj) {
          if (ZeroSeedExtension) {
            std::vector<unsigned char> &values = si.assignment.bindings[array];
            values = std::vector<unsigned char>(mo->size, '\0');
          } else if (!AllowSeedExtension) {
            terminateStateOnError(state, 
                                  "ran out of inputs during seeding",
                                  "user.err");
            break;
          }
        } else {
          if (obj->numBytes != mo->size &&
              ((!(AllowSeedExtension || ZeroSeedExtension)
                && obj->numBytes < mo->size) ||
               (!AllowSeedTruncation && obj->numBytes > mo->size))) {
	    std::stringstream msg;
	    msg << "replace size mismatch: "
		<< mo->name << "[" << mo->size << "]"
		<< " vs " << obj->name << "[" << obj->numBytes << "]"
		<< " in test\n";

            terminateStateOnError(state,
                                  msg.str(),
                                  "user.err");
            break;
          } else {
            std::vector<unsigned char> &values = si.assignment.bindings[array];
            values.insert(values.begin(), obj->bytes, 
                          obj->bytes + std::min(obj->numBytes, mo->size));
            if (ZeroSeedExtension) {
              for (unsigned i=obj->numBytes; i<mo->size; ++i)
                values.push_back('\0');
            }
          }
        }
      }
    }
  } else {
    ObjectState *os = bindObjectInState(state, mo, false);
    if (replayPosition >= replayOut->numObjects) {
      terminateStateOnError(state, "replay count mismatch", "user.err");
    } else {
      KTestObject *obj = &replayOut->objects[replayPosition++];
      if (obj->numBytes != mo->size) {
        terminateStateOnError(state, "replay size mismatch", "user.err");
      } else {
        for (unsigned i=0; i<mo->size; i++)
          os->write8(i, obj->bytes[i]);
      }
    }
  }
}

/***/

void Executor::runFunctionAsMain(Function *f,
				 int argc,
				 char **argv,
				 char **envp) {
  std::vector<ref<Expr> > arguments;

  // force deterministic initialization of memory objects
  //srand(1);
  //srandom(1);
  
  MemoryObject *argvMO = 0;

  // In order to make uclibc happy and be closer to what the system is
  // doing we lay out the environments at the end of the argv array
  // (both are terminated by a null). There is also a final terminating
  // null that uclibc seems to expect, possibly the ELF header?

  int envc;
  for (envc=0; envp[envc]; ++envc) ;

  unsigned NumPtrBytes = Context::get().getPointerWidth() / 8;
  KFunction *kf = kmodule->functionMap[f];
  assert(kf);
  Function::arg_iterator ai = f->arg_begin(), ae = f->arg_end();
  if (ai!=ae) {
    arguments.push_back(ConstantExpr::alloc(argc, Expr::Int32));

    if (++ai!=ae) {
      argvMO = memory->allocate((argc+1+envc+1+1) * NumPtrBytes, false, true,
                                f->begin()->begin());
      
      arguments.push_back(argvMO->getBaseExpr());

      if (++ai!=ae) {
        uint64_t envp_start = argvMO->address + (argc+1)*NumPtrBytes;
        arguments.push_back(Expr::createPointer(envp_start));

        if (++ai!=ae)
          klee_error("invalid main function (expect 0-3 arguments)");
      }
    }
  }

  sharedAddrSpace = new AddressSpace();
  ExecutionState *state = new ExecutionState(kmodule->functionMap[f]);
  state->pid = gettid();
  state->stateInWindow = 0;
  state->pthreadCreateStackDepth = 0;
  state->threadLocalWindowSerialNum = 0;
  
  if (pathWriter) 
    state->pathOS = pathWriter->open();
  if (symPathWriter) 
    state->symPathOS = symPathWriter->open();

/*
  if (statsTracker)
    statsTracker->framePushed(*state, 0);
*/

  assert(arguments.size() == f->arg_size() && "wrong number of arguments");
  for (unsigned i = 0, e = f->arg_size(); i != e; ++i) {
    bindArgument(kf, i, *state, arguments[i]);

    //Xiaowei
    //writeShdwReg(kf, i, *state, NULL);
  }

  if (argvMO) {
    ObjectState *argvOS = bindObjectInState(*state, argvMO, false);

    for (int i=0; i<argc+1+envc+1+1; i++) {
      MemoryObject *arg;
      
      if (i==argc || i>=argc+1+envc) {
        arg = 0;
      } else {
        char *s = i<argc ? argv[i] : envp[i-(argc+1)];
        int j, len = strlen(s);
        
        arg = memory->allocate(len+1, false, true, state->pc->inst);
        ObjectState *os = bindObjectInState(*state, arg, false);
        for (j=0; j<len+1; j++)
          os->write8(j, s[j]);
      }

      if (arg) {
        argvOS->write(i * NumPtrBytes, arg->getBaseExpr());
        argvOS->writeConcrete(i * NumPtrBytes, arg->getBaseExpr());
      } else {
        argvOS->write(i * NumPtrBytes, Expr::createPointer(0));
        argvOS->writeConcrete(i * NumPtrBytes, Expr::createPointer(0));
      }
    }
  }
  
  initializeGlobals(*state);

//  processTree = new PTree(state);
//  state->ptreeNode = processTree->root;

  // YJF: load options for record
  load_options("local.options");

#ifdef MEMOIZER_ORDER
  memoizer->appStart();
  if (IS_BATCH_PROGRAM) {
    memoizer->taskStart(&(state->threadLocalWindowSerialNum), 0, 0, NULL, 0, NULL);
  }
#endif

  run(*state);
/*  delete processTree;
  processTree = 0;

  // hack to clear memory objects
  delete memory;
  memory = new MemoryManager();
  
  globalObjects.clear();
  globalAddresses.clear();

  if (statsTracker)
    statsTracker->done();

  if (theMMap) {
    munmap(theMMap, theMMapSize);
    theMMap = 0;
  }*/
}

unsigned Executor::getPathStreamID(const ExecutionState &state) {
  assert(pathWriter);
  return state.pathOS.getID();
}

unsigned Executor::getSymbolicPathStreamID(const ExecutionState &state) {
  assert(symPathWriter);
  return state.symPathOS.getID();
}

void Executor::getConstraintLog(const ExecutionState &state,
                                std::string &res,
                                bool asCVC) {
  if (asCVC) {
    Query query(state.constraints, ConstantExpr::alloc(0, Expr::Bool));
    char *log = solver->stpSolver->getConstraintLog(query);
    res = std::string(log);
    free(log);
  } else {
    std::ostringstream info;
    ExprPPrinter::printConstraints(info, state.constraints);
    res = info.str();    
  }
}

bool Executor::getSymbolicSolution(const ExecutionState &state,
                                   std::vector< 
                                   std::pair<std::string,
                                   std::vector<unsigned char> > >
                                   &res) {
  solver->setTimeout(stpTimeout);

  ExecutionState tmp(state);
  if (!NoPreferCex) {
    for (unsigned i = 0; i != state.symbolics.size(); ++i) {
      const MemoryObject *mo = state.symbolics[i].first;
      std::vector< ref<Expr> >::const_iterator pi = 
        mo->cexPreferences.begin(), pie = mo->cexPreferences.end();
      for (; pi != pie; ++pi) {
        bool mustBeTrue;
        bool success = solver->mustBeTrue(tmp, Expr::createIsZero(*pi), 
                                          mustBeTrue);
        if (!success) break;
        if (!mustBeTrue) tmp.addConstraint(*pi);
      }
      if (pi!=pie) break;
    }
  }

  std::vector< std::vector<unsigned char> > values;
  std::vector<const Array*> objects;
  for (unsigned i = 0; i != state.symbolics.size(); ++i)
    objects.push_back(state.symbolics[i].second);
  bool success = solver->getInitialValues(tmp, objects, values);
  solver->setTimeout(0);
  if (!success) {
    klee_warning("unable to compute initial values (invalid constraints?)!");
    ExprPPrinter::printQuery(std::cerr,
                             state.constraints, 
                             ConstantExpr::alloc(0, Expr::Bool));
    return false;
  }
  
  for (unsigned i = 0; i != state.symbolics.size(); ++i)
    res.push_back(std::make_pair(state.symbolics[i].first->name, values[i]));
  return true;
}

void Executor::getCoveredLines(const ExecutionState &state,
                               std::map<const std::string*, std::set<unsigned> > &res) {
  res = state.coveredLines;
}

void Executor::doImpliedValueConcretization(ExecutionState &state,
                                            ref<Expr> e,
                                            ref<ConstantExpr> value) {
  abort(); // FIXME: Broken until we sort out how to do the write back.

  if (DebugCheckForImpliedValues)
    ImpliedValue::checkForImpliedValues(solver->solver, e, value);

  ImpliedValueList results;
  ImpliedValue::getImpliedValues(e, value, results);
  for (ImpliedValueList::iterator it = results.begin(), ie = results.end();
       it != ie; ++it) {
    ReadExpr *re = it->first.get();
    
    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(re->index)) {
      // FIXME: This is the sole remaining usage of the Array object
      // variable. Kill me.
      const MemoryObject *mo = 0; //re->updates.root->object;
      const ObjectState *os = state.addressSpace.findObject(mo);

      if (!os) {
        // object has been free'd, no need to concretize (although as
        // in other cases we would like to concretize the outstanding
        // reads, but we have no facility for that yet)
      } else {
        assert(!os->readOnly && 
               "not possible? read only object with static read?");
        long int_os2 = (long)os;
	    ObjectState *os2 = (ObjectState *)int_os2;
        ObjectState *wos = state.addressSpace.getWriteable(mo, os2);
        wos->write(CE, it->second);
      }
    }
  }
}

Expr::Width Executor::getWidthForLLVMType(const llvm::Type *type) const {
  return kmodule->targetData->getTypeSizeInBits(type);
}

bool Executor::states_empty() {
  int tid = gettid();
	
  for (Tid_To_State_Map::iterator it = hashStates.begin(), ie = hashStates.end(); it != ie; ++it) {
    ExecutionState *es = it->second;
    if (es->pid == tid) {
      return false;
    }
  }
  return true;
}

// Heming: we handle fork, mmap, munmap functions so far which KLEE does not handle.
void Executor::ternHandleSpecialFunctions(ExecutionState &state, const char *funcName, const uint64_t *args) {
  if (strcmp(funcName, "fork") == 0 && args[0] == 0) {
    updateStatesForChildProcess();
  } else if (strcmp(funcName, "mmap") == 0 && args[0] != 0 && (int)args[0] != -1) {
    MemoryObject *mo = memory->allocateFixed(args[0], args[3], 0);	// Heming: make allocateSite to 0 temporarilly.
    /*ObjectState *os = */bindObjectInState(state, mo, false);
//	fprintf(stderr, "KLEE: Pid %d mmap start addr %llx, size %llu\n", getpid(), args[0], args[3]);
  } else if (strcmp(funcName, "munmap") == 0 && args[0] == 0) {
    MemoryObject mo(args[2]);
    const ObjectState *os = state.addressSpace.findObject(&mo);
    if (os->size != (unsigned)args[3]) {
      assert(false && "TERN munmap must un map the same size as mmap!");
    	}
	state.addressSpace.unbindObject(&mo);
	//fprintf(stderr, "KLEE: Pid %d munmap start addr %llx, size %llu\n", getpid(), args[2], args[3]);
  }
}

void Executor::updateStatesForChildProcess() {
  fprintf(stderr, "Pid %d updateStatesForChildProcess\n", getpid());
  int match = 0;
	
  for (Tid_To_State_Map::iterator it = hashStates.begin(), ie = hashStates.end(); it != ie; ++it) {
      ExecutionState *es = it->second;
      assert(es != NULL);
	if (es->pid == getppid()) {
		es->pid = getpid();
	 	match++;
	}
  }

  assert(match == 1);
  assert(hashStates[getppid()]);
  hashStates[gettid()] = hashStates[getppid()];
  assert(hashStates.erase(getppid()));
#ifdef MEMOIZER_ORDER
  memoizer->updateTidMapForFork(getppid(), getpid());
#endif
  fprintf(stderr, "Pid %d updateStatesForChildProcess End\n", getpid());
}

void Executor::printKLEECallStack(ExecutionState &state) {
  BasicBlock *BB = state.prevPC->inst->getParent();
  BasicBlock::iterator IB = BB->begin();
  BasicBlock::iterator IE = BB->end();
		
  /*while (IB != IE) {
    Instruction *I = IB;
    errs() << "Inst " << *I << "\n";
    IB++;
  }*/
	
  int inst_id = exeInstIDs[(long)(state.prevPC->inst)];
  fprintf(stderr, "printKLEECallStack for state with tid %d, inst id %d: ", state.pid, inst_id);
  for (unsigned i = 0; i < state.stack.size(); i++) {
    StackFrame &sf = state.stack.at(i);
    assert(sf.kf->function->hasName());
    fprintf(stderr, "%s, ", sf.kf->function->getNameStr().c_str());
  }
  fprintf(stderr, "\n\n\n");
  state.addressSpace.printAddrSpace();
}

void Executor::initInstMapAndModule(Module *module, Memoizer *mmz, SchedCache *sc, Slicer *slr) {
  PassManager pm;
  InsertSubroutinePass *ISP = new InsertSubroutinePass();
  pm.add(ISP);
  pm.run(*module);
  exeInstIDs = ISP->getInstMap();
  memoizer = mmz;
  schedCache = sc;
  //Xiaowei:
  slicer = slr;
}

Memoizer *Executor::getMemoizer() {
	return memoizer;
}
void Executor::ternInstCntStat(ExecutionState &state) {
	instCount++;
	if (instCount%INST_CNT_INTERVAL == 0) {
		fprintf(stderr, "[%llu], ", (unsigned long long)instCount);
	}
	if (instCount%(INST_CNT_INTERVAL*10) == 0) {
		fprintf(stderr, "\n");
		printKLEECallStack(state);
	}
}

// Return true, means executed successfully.
bool Executor::fastExecutionForMemOps(const char *funcName, ExecutionState &state, KInstruction *ki, Function *f, std::vector< ref<Expr> > &concreteArguments) {
	// Interpret the memcpy within the Executor instead of interpreting each llvm instruction in the memcpy function. This could make KLEE much faster.
	if (strcmp(funcName, "memcpy") == 0) {
		if (!isa<ConstantExpr>(concreteArguments[0]) || !isa<ConstantExpr>(concreteArguments[1]) || !isa<ConstantExpr>(concreteArguments[2])) {
			fprintf(stderr, "Executor::fastExecutionForMemOps switches back to slow path1\n");
			return false;
		}

		unsigned toOffset;
		ObjectState *toMemObj = getMemObjectByAddr(state, concreteArguments[0], toOffset);
		unsigned fromOffset;
		ObjectState *fromMemObj = getMemObjectByAddr(state, concreteArguments[1], fromOffset);
		if (toMemObj == NULL)
			return false;
		if (fromMemObj == NULL)
			return false;

		unsigned cpSize = (unsigned)cast<ConstantExpr>(concreteArguments[2])->getZExtValue();
		unsigned fromBound = (fromOffset + cpSize) < fromMemObj->size ? (fromOffset + cpSize) : fromMemObj->size;

		/*fprintf(stderr, "\n\n\nKLEE::Executor forces %s to be fastExecutionForMemOps arg: %llx, %llx, %llx, toOffset %u/%u, fromOffset %u/%u\n\n\n", 
			funcName, cast<ConstantExpr>(concreteArguments[0])->getZExtValue(),
			cast<ConstantExpr>(concreteArguments[1])->getZExtValue(), cast<ConstantExpr>(concreteArguments[2])->getZExtValue(),
			toOffset, toBound, fromOffset, fromBound);*/

		/* Do the memcpy operation as an external function, remember that this function only do the copy of concreate bytes,
			we still need to copy the symbolic bytes and update flags for toMemory. 
			We call this function since we need to build the return value for memcpy(). */
		// If do not call this function like this, dbt2 can not connect to klee+mysqld.bc, weird.
		callExternalFunction(state, ki, f, concreteArguments);

		// copy the symbolic bytes and update flags for toMemory.
		unsigned offset = toOffset;
		for (unsigned i = fromOffset; i < fromBound; i++) {
			if (fromMemObj->isByteConcrete(i)) {
				toMemObj->write8(offset, fromMemObj->read8ConcreteStore(i));
			} else {
				toMemObj->write8(offset, fromMemObj->read8(i));
			}
			offset++;
		}
		
		//fprintf(stderr, "Executor::fastExecutionForMemOps returns true!\n");
		return true;
	}

	if (strcmp(funcName, "strlen") == 0) {
		// TODO:
	}
		
	return false;
}

ObjectState *Executor::getMemObjectByAddr(ExecutionState &state, ref<Expr> address, unsigned &memOffset) {
  // fast path: single in-bounds resolution
  ObjectPair op;
  bool success = true;

  if (!isa<ConstantExpr>(address))
    return NULL;

  solver->setTimeout(stpTimeout);
  if (!state.addressSpace.resolveOne(state, solver, address, op, success)) {
    solver->setTimeout(0);
    return NULL;
  }
  solver->setTimeout(0);

  // Heming added this: if use tree search, fail, then we just use linear search to the address space.
  if (!success) {
      uint64_t addr = cast<ConstantExpr>(address)->getZExtValue();
      fprintf(stderr, "Tid %d failed and findObject can not got it %llx\n", gettid(), addr);
	  return NULL;
  } else {
    const MemoryObject *mo = op.first;
    ref<Expr> offset = mo->getOffsetExpr(address);
	assert(isa<ConstantExpr>(offset));
	memOffset = (unsigned)cast<ConstantExpr>(offset)->getZExtValue();
	const ObjectState *os = op.second;
	long intOs = (long)os;
	return (ObjectState *)intOs;
  }
}

///

Interpreter *Interpreter::create(const InterpreterOptions &opts,
                                 InterpreterHandler *ih) {
  return new Executor(opts, ih);
}
